Symbolic tracing

runtime/CMakeLists.txt

@@ -34,6 +34,7 @@ set(SHARED_RUNTIME_SOURCES
   ${CMAKE_CURRENT_SOURCE_DIR}/RuntimeCommon.cpp
   ${CMAKE_CURRENT_SOURCE_DIR}/LibcWrappers.cpp
   ${CMAKE_CURRENT_SOURCE_DIR}/Shadow.cpp
+  ${CMAKE_CURRENT_SOURCE_DIR}/Tracer.cpp
   ${CMAKE_CURRENT_SOURCE_DIR}/GarbageCollection.cpp)
 
 if (${QSYM_BACKEND})

runtime/GarbageCollection.cpp

@@ -23,6 +23,10 @@
 /// A list of memory regions that are known to contain symbolic expressions.
 std::vector<ExpressionRegion> expressionRegions;
 
+std::vector<ExpressionRegion>& getExpressionRegions() {
+  return expressionRegions;
+}
+
 void registerExpressionRegion(ExpressionRegion r) {
   expressionRegions.push_back(std::move(r));
 }

runtime/GarbageCollection.h

@@ -28,6 +28,7 @@ using ExpressionRegion = std::pair<SymExpr *, size_t>;
 /// Add the specified region to the list of places to search for symbolic
 /// expressions.
 void registerExpressionRegion(ExpressionRegion r);
+std::vector<ExpressionRegion>& getExpressionRegions();
 
 /// Return the set of currently reachable symbolic expressions.
 std::set<SymExpr> collectReachableExpressions();

runtime/RuntimeCommon.cpp

@@ -27,6 +27,7 @@
 #include "GarbageCollection.h"
 #include "RuntimeCommon.h"
 #include "Shadow.h"
+#include "Tracer.h"
 
 namespace {
 
@@ -486,3 +487,10 @@ SymExpr _sym_build_bit_to_bool(SymExpr expr) {
   return _sym_build_not_equal(expr,
                               _sym_build_integer(0, _sym_bits_helper(expr)));
 }
+
+void _sym_trace_execution(uintptr_t pc) { Tracer::traceStep(pc);
+}
+
+void _sym_finalize_tracing() {
+  Tracer::writeTraceToDisk();
+}

runtime/RuntimeCommon.h

@@ -211,6 +211,8 @@ void _sym_notify_basic_block(uintptr_t site_id);
  */
 const char *_sym_expr_to_string(SymExpr expr); // statically allocated
 bool _sym_feasible(SymExpr expr);
+void _sym_trace_execution(uintptr_t pc);
+void _sym_finalize_tracing(void);
 
 /*
  * Garbage collection

runtime/Tracer.cpp

@@ -0,0 +1,113 @@
+
+#include "Tracer.h"
+#include "Shadow.h"
+#include "llvm/Support/raw_ostream.h"
+
+nlohmann::json Tracer::currentTrace;
+nlohmann::json Tracer::expressions;
+nlohmann::json Tracer::pathConstraints;
+const std::string Tracer::BACKEND_TRACE_FILE = "/tmp/backend_trace.json";
+
+void Tracer::traceStep(uintptr_t pc) {
+
+  nlohmann::json newEntry;
+  newEntry["pc"] = pc;
+  newEntry["memory_to_expression_mapping"] = nlohmann::json::object();
+
+  /* dump shadow pages */
+  for (auto const &[pageAddress, _] : g_shadow_pages) {
+    for (auto byteAddress = pageAddress; byteAddress < pageAddress + kPageSize;
+         byteAddress++) {
+      auto byteExpr = _sym_read_memory((u_int8_t *)byteAddress, 1, true);
+      if (byteExpr != nullptr && !byteExpr->isConcrete()) {
+
+        newEntry["memory_to_expression_mapping"][std::to_string(reinterpret_cast<uintptr_t>(byteAddress))] =
+                    getExpressionID(byteExpr);
+      }
+    }
+  }
+
+  /* dump regions that the client has registered with _sym_register_expression_region
+   * for SymQEMU, this is env_exprs which contains the expressions for the global TCG variables (i.e., guest registers) */
+  for (auto &expressionRegion : getExpressionRegions()){
+    for (auto byteAddress = expressionRegion.first; byteAddress < expressionRegion.first + expressionRegion.second / sizeof(byteAddress);
+         byteAddress++) {
+      auto byteExpr = *byteAddress;
+      if (byteExpr != nullptr && !byteExpr->isConcrete()) {
+
+        newEntry["memory_to_expression_mapping"][std::to_string(reinterpret_cast<uintptr_t>(byteAddress))] =
+                    getExpressionID(byteExpr);
+      }
+    }
+  }
+
+  currentTrace.push_back(newEntry);
+}
+
+
+void Tracer::tracePathConstraint(SymExpr constraint, bool taken) {
+  if (pathConstraints.empty()) {
+     symcc_set_test_case_handler(
+        reinterpret_cast<TestCaseHandler>(traceNewInput));
+  }
+
+  nlohmann::json newEntry;
+  newEntry["expression"] = getExpressionID(constraint);
+  newEntry["after_step"] = currentTrace.size() - 1;
+  newEntry["new_input_value"] = nlohmann::json();
+  newEntry["taken"] = taken;
+
+  pathConstraints.push_back(newEntry);
+}
+
+void Tracer::traceNewInput(const unsigned char *input, size_t size) {
+  for (size_t i = 0; i < size; i++) {
+    pathConstraints[pathConstraints.size() - 1]["new_input_value"].push_back(
+        input[i]);
+  }
+}
+
+void Tracer::writeTraceToDisk() {
+  for (auto const &[_, expressionPtr] : getAllocatedExpressions()) {
+    recursivelyCollectExpressions(expressionPtr);
+  }
+
+  nlohmann::json dataToSave;
+  dataToSave["trace"] = currentTrace;
+  dataToSave["expressions"] = expressions;
+  dataToSave["path_constraints"] = pathConstraints;
+
+  std::ofstream o(BACKEND_TRACE_FILE);
+  o << std::setw(4) << dataToSave << std::endl;
+}
+
+void Tracer::recursivelyCollectExpressions(const shared_ptr<qsym::Expr>&expressionPtr) {
+  string expressionID = getExpressionID(expressionPtr.get());
+  if (expressions.count(expressionID) > 0) {
+    return;
+  }
+
+  expressions[expressionID]["operation"]["kind"] = expressionPtr->kind();
+  expressions[expressionID]["operation"]["properties"] = nlohmann::json::object();
+  if (expressionPtr->kind() == qsym::Constant){
+    auto value_llvm_int = static_pointer_cast<qsym::ConstantExpr>(expressionPtr)->value();
+    std::string value_str;
+    llvm::raw_string_ostream rso(value_str);
+    value_llvm_int.print(rso, false);
+
+    expressions[expressionID]["operation"]["properties"]["value"] = value_str;
+  }
+  expressions[expressionID]["size_bits"] = expressionPtr->bits();
+  expressions[expressionID]["input_byte_dependency"] = *expressionPtr->getDependencies();
+  expressions[expressionID]["args"] = nlohmann::json::array();
+  for (int child_i = 0; child_i < expressionPtr->num_children(); child_i++) {
+    shared_ptr<qsym::Expr> child = expressionPtr->getChild(child_i);
+    string childID = getExpressionID(child.get());
+    expressions[expressionID]["args"].push_back(childID);
+    recursivelyCollectExpressions(child);
+  }
+}
+
+string Tracer::getExpressionID(SymExpr expression) {
+  return std::to_string(reinterpret_cast<uintptr_t>(expression));
+}

runtime/Tracer.h

@@ -0,0 +1,58 @@
+
+#ifndef SYMRUNTIME_TRACER_H
+#define SYMRUNTIME_TRACER_H
+
+#include "GarbageCollection.h"
+#include "Runtime.h"
+#include <cstdint>
+#include <fstream>
+#include <nlohmann/json.hpp>
+
+/**
+ * Generates a trace of the symbolic execution.
+ *
+ * A trace contains a list of symbolic memory snapshots, a list of path constraints and a list of expressions.
+ * The trace is written to a json file at the end of the execution.
+ */
+class Tracer {
+public:
+  /**
+   * Adds a dump of the current symbolic state to the trace.
+   */
+  static void traceStep(uintptr_t pc);
+
+  /**
+   * Adds a path constraint to the trace.
+   */
+  static void tracePathConstraint(SymExpr constraint, bool taken);
+
+  /**
+   * Adds an input generated by the symbolic backend.
+   * The input is associated to the last path constraint.
+   */
+  static void traceNewInput(const unsigned char* input, size_t size);
+
+  /**
+   * Generates a json file containing the trace.
+   * Must be called before the program exits.
+   */
+  static void writeTraceToDisk();
+
+private:
+  /**
+   * Collects all expressions reachable from the given expression.
+   */
+  static void recursivelyCollectExpressions(const shared_ptr<qsym::Expr>&expressionPtr);
+
+  /**
+   * Generates a string ID from the address of the given expression.
+   */
+  static string getExpressionID(SymExpr expression);
+
+  static nlohmann::json currentTrace;
+  static nlohmann::json expressions;
+  static nlohmann::json pathConstraints;
+  static const std::string BACKEND_TRACE_FILE;
+};
+
+#endif // SYMRUNTIME_TRACER_H

runtime/qsym_backend/CMakeLists.txt

@@ -83,7 +83,13 @@ target_include_directories(SymRuntime SYSTEM PRIVATE
 # We need to get the LLVM support component for llvm::APInt.
 llvm_map_components_to_libnames(QSYM_LLVM_DEPS support)
 
-target_link_libraries(SymRuntime ${Z3_LIBRARIES} ${QSYM_LLVM_DEPS})
+include(FetchContent)
+
+FetchContent_Declare(json URL https://github.com/nlohmann/json/releases/download/v3.11.2/json.tar.xz)
+FetchContent_MakeAvailable(json)
+
+
+target_link_libraries(SymRuntime ${Z3_LIBRARIES} ${QSYM_LLVM_DEPS} nlohmann_json::nlohmann_json)
 
 # 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

runtime/qsym_backend/Runtime.cpp

@@ -19,6 +19,7 @@
 
 #include "Runtime.h"
 #include "GarbageCollection.h"
+#include "Tracer.h"
 
 // C++
 #if __has_include(<filesystem>)
@@ -154,6 +155,10 @@ EnhancedQsymSolver *g_enhanced_solver;
 
 } // namespace
 
+std::map<SymExpr, qsym::ExprRef> &getAllocatedExpressions() {
+  return allocatedExpressions;
+}
+
 using namespace qsym;
 
 #if HAVE_FILESYSTEM
@@ -321,6 +326,7 @@ void _sym_push_path_constraint(SymExpr constraint, int taken,
   if (constraint == nullptr)
     return;
 
+  Tracer::tracePathConstraint(constraint, taken != 0);
   g_solver->addJcc(allocatedExpressions.at(constraint), taken != 0, site_id);
 }
 
@@ -449,7 +455,7 @@ bool _sym_feasible(SymExpr expr) {
 //
 
 void _sym_collect_garbage() {
-  if (allocatedExpressions.size() < g_config.garbageCollectionThreshold)
+//  if (allocatedExpressions.size() < g_config.garbageCollectionThreshold)
     return;
 
 #ifdef DEBUG_RUNTIME

runtime/qsym_backend/Runtime.h

@@ -21,4 +21,6 @@
 typedef qsym::Expr *SymExpr;
 #include <RuntimeCommon.h>
 
+std::map<SymExpr, qsym::ExprRef> &getAllocatedExpressions();
+
 #endif

util/symbolic_trace/.gitignore

@@ -0,0 +1,4 @@
+build
+symcctrace.egg-info
+.idea
+__pycache__

util/symbolic_trace/README.md

@@ -0,0 +1,7 @@
+This is a python package for parsing a trace generated by the tracing feature of SymCC.
+
+Install it with
+
+```
+pip install .
+```

util/symbolic_trace/pyproject.toml

@@ -0,0 +1,3 @@
+[project]
+name = "symcctrace"
+version = "1.0"

util/symbolic_trace/symcctrace/__init__.py

@@ -0,0 +1,2 @@
+from .parsing import parse_trace
+from .data import TraceData