Add --mutable-bytes flag to enable possibly unsound optimizations (#…

…962)

This PR adds a flag to `llvm-kompile` that enables semantics used by the
LLVM backend that are unsound in certain scenarios, but are useful for
performance (making objects of sort `Bytes` copy-on-write rather than
mutable).

The numerous edge cases from my initial attempt to fix this issue in
#950 are retained as test cases here.

Fixes #930 

Blocked until we have propagated
runtimeverification/k#3934 appropriately to
downstream semantics.

bin/llvm-kompile

@@ -34,6 +34,9 @@ Options:
                                be called from kompile. Only meaningful in "c" mode.
   -fno-omit-frame-pointer      Keep the frame pointer in compiled code for debugging purposes.
   --proof-hint-instrumentation Enable instrumentation for generation of proof hints.
+  --mutable-bytes              Use the faster, unsound (mutable) semantics for objects of sort
+                               Bytes at run time, rather than the slower, sound
+                               (immutable) that are enabled by default.
   -O[0123]                     Set the optimization level for code generation.
 
 Any option not listed above will be passed through to clang; use '--' to
@@ -167,6 +170,10 @@ while [[ $# -gt 0 ]]; do
       codegen_flags+=("--proof-hint-instrumentation")
       shift
       ;;
+    --mutable-bytes)
+      codegen_flags+=("--mutable-bytes")
+      shift
+      ;;
     -O*)
       codegen_flags+=("$1")
       kompile_clang_flags+=("$1")

bindings/c/include/kllvm-c/kllvm-c.h

@@ -158,6 +158,10 @@ void kore_symbol_add_formal_argument(kore_symbol *, kore_sort const *);
 void kllvm_init(void);
 void kllvm_free_all_memory(void);
 
+/* Sort-specific functions */
+
+bool kllvm_mutable_bytes_enabled(void);
+
 #ifdef __cplusplus
 }
 #endif

bindings/c/lib.cpp

@@ -67,8 +67,9 @@ auto managed(kore_symbol *ptr) {
  */
 
 extern "C" {
-void initStaticObjects(void);
-void freeAllKoreMem(void);
+void initStaticObjects();
+void freeAllKoreMem();
+bool hook_BYTES_mutableBytesEnabled();
 }
 
 extern "C" {
@@ -426,6 +427,10 @@ void kllvm_init(void) {
 void kllvm_free_all_memory(void) {
   freeAllKoreMem();
 }
+
+bool kllvm_mutable_bytes_enabled(void) {
+  return hook_BYTES_mutableBytesEnabled();
+}
 }
 
 namespace {

include/kllvm/codegen/CreateTerm.h

@@ -82,9 +82,6 @@ std::string escape(std::string const &str);
    llvm modules in the llvm backend. */
 std::unique_ptr<llvm::Module>
 newModule(std::string const &name, llvm::LLVMContext &Context);
-void addKompiledDirSymbol(
-    llvm::LLVMContext &Context, std::string const &dir, llvm::Module *mod,
-    bool debug);
 
 llvm::StructType *getBlockType(
     llvm::Module *Module, KOREDefinition *definition, KORESymbol const *symbol);

include/kllvm/codegen/Metadata.h

@@ -0,0 +1,18 @@
+#ifndef KLLVM_CODEGEN_H
+#define KLLVM_CODEGEN_H
+
+#include <llvm/IR/LLVMContext.h>
+#include <llvm/IR/Module.h>
+
+#include <string>
+
+namespace kllvm {
+
+void addKompiledDirSymbol(
+    llvm::Module &mod, std::string const &dir, bool debug);
+
+void addMutableBytesFlag(llvm::Module &mod, bool enabled, bool debug);
+
+} // namespace kllvm
+
+#endif

lib/codegen/CMakeLists.txt

@@ -6,6 +6,7 @@ add_library(Codegen
   Decision.cpp
   DecisionParser.cpp
   EmitConfigParser.cpp
+  Metadata.cpp
   Options.cpp
   ProofEvent.cpp
   Util.cpp

lib/codegen/CreateTerm.cpp

@@ -129,23 +129,6 @@ newModule(std::string const &name, llvm::LLVMContext &Context) {
   return mod;
 }
 
-static std::string KOMPILED_DIR = "kompiled_directory";
-
-void addKompiledDirSymbol(
-    llvm::LLVMContext &Context, std::string const &dir, llvm::Module *mod,
-    bool debug) {
-  auto *Str = llvm::ConstantDataArray::getString(Context, dir, true);
-  auto *global = mod->getOrInsertGlobal(KOMPILED_DIR, Str->getType());
-  auto *globalVar = llvm::cast<llvm::GlobalVariable>(global);
-  if (!globalVar->hasInitializer()) {
-    globalVar->setInitializer(Str);
-  }
-
-  if (debug) {
-    initDebugGlobal(KOMPILED_DIR, getCharDebugType(), globalVar);
-  }
-}
-
 std::string MAP_STRUCT = "map";
 std::string RANGEMAP_STRUCT = "rangemap";
 std::string LIST_STRUCT = "list";

lib/codegen/Metadata.cpp

@@ -0,0 +1,50 @@
+#include <kllvm/codegen/Debug.h>
+#include <kllvm/codegen/Metadata.h>
+
+#include <llvm/IR/Constants.h>
+#include <llvm/IR/LLVMContext.h>
+#include <llvm/IR/Module.h>
+#include <llvm/IR/Type.h>
+
+namespace kllvm {
+
+static std::string KOMPILED_DIR = "kompiled_directory";
+static std::string STRICT_BYTES = "enable_mutable_bytes";
+
+void addKompiledDirSymbol(
+    llvm::Module &mod, std::string const &dir, bool debug) {
+  auto &ctx = mod.getContext();
+
+  auto *str = llvm::ConstantDataArray::getString(ctx, dir, true);
+
+  auto *global = mod.getOrInsertGlobal(KOMPILED_DIR, str->getType());
+  auto *global_var = llvm::cast<llvm::GlobalVariable>(global);
+
+  if (!global_var->hasInitializer()) {
+    global_var->setInitializer(str);
+  }
+
+  if (debug) {
+    initDebugGlobal(KOMPILED_DIR, getCharDebugType(), global_var);
+  }
+}
+
+void addMutableBytesFlag(llvm::Module &mod, bool enabled, bool debug) {
+  auto &ctx = mod.getContext();
+
+  auto *i1_ty = llvm::Type::getInt1Ty(ctx);
+  auto *enabled_cst = llvm::ConstantInt::getBool(ctx, enabled);
+
+  auto *global = mod.getOrInsertGlobal(STRICT_BYTES, i1_ty);
+  auto *global_var = llvm::cast<llvm::GlobalVariable>(global);
+
+  if (!global_var->hasInitializer()) {
+    global_var->setInitializer(enabled_cst);
+  }
+
+  if (debug) {
+    initDebugGlobal(STRICT_BYTES, getBoolDebugType(), global_var);
+  }
+}
+
+} // namespace kllvm

runtime/strings/CMakeLists.txt

@@ -1,6 +1,7 @@
 add_library(strings STATIC
   strings.cpp
   bytes.cpp
+  copy_on_write.cpp
 )
 
 target_link_libraries(strings

runtime/strings/bytes.cpp

@@ -4,10 +4,13 @@
 #include <cstring>
 #include <gmp.h>
 #include <stdexcept>
+#include <unordered_set>
 
 #include "runtime/alloc.h"
 #include "runtime/header.h"
 
+void copy_if_needed(SortBytes &b);
+
 extern "C" {
 
 #undef get_ui
@@ -153,6 +156,8 @@ SortInt hook_BYTES_get(SortBytes b, SortInt off) {
 }
 
 SortBytes hook_BYTES_update(SortBytes b, SortInt off, SortInt val) {
+  copy_if_needed(b);
+
   unsigned long off_long = get_ui(off);
   if (off_long >= len(b)) {
     KLLVM_HOOK_INVALID_ARGUMENT(
@@ -168,6 +173,8 @@ SortBytes hook_BYTES_update(SortBytes b, SortInt off, SortInt val) {
 }
 
 SortBytes hook_BYTES_replaceAt(SortBytes b, SortInt start, SortBytes b2) {
+  copy_if_needed(b);
+
   unsigned long start_long = get_ui(start);
   if (start_long + len(b2) > len(b)) {
     KLLVM_HOOK_INVALID_ARGUMENT(
@@ -180,6 +187,8 @@ SortBytes hook_BYTES_replaceAt(SortBytes b, SortInt start, SortBytes b2) {
 
 SortBytes
 hook_BYTES_memset(SortBytes b, SortInt start, SortInt count, SortInt value) {
+  copy_if_needed(b);
+
   uint64_t ustart = get_ui(start);
   uint64_t ucount = get_ui(count);
   uint64_t uend = ustart + ucount;
@@ -244,6 +253,7 @@ SortBytes hook_BYTES_padLeft(SortBytes b, SortInt length, SortInt v) {
 }
 
 SortBytes hook_BYTES_reverse(SortBytes b) {
+  copy_if_needed(b);
   std::reverse(b->data, b->data + len(b));
   return b;
 }

runtime/strings/copy_on_write.cpp

@@ -0,0 +1,25 @@
+#include <runtime/header.h>
+
+extern "C" bool enable_mutable_bytes;
+
+namespace {
+
+SortBytes copy_bytes(SortBytes b) {
+  auto new_len = len(b);
+  auto *ret = static_cast<string *>(koreAllocToken(sizeof(string) + new_len));
+  init_with_len(ret, new_len);
+  memcpy(&(ret->data), &(b->data), new_len * sizeof(char));
+  return ret;
+}
+
+} // namespace
+
+extern "C" bool hook_BYTES_mutableBytesEnabled() {
+  return enable_mutable_bytes;
+}
+
+void copy_if_needed(SortBytes &b) {
+  if (!hook_BYTES_mutableBytesEnabled()) {
+    b = copy_bytes(b);
+  }
+}

test/c/Inputs/api.c

@@ -62,6 +62,7 @@ struct kllvm_c_api load_c_api(char const *path) {
   API_FUNCTION(kore_symbol_add_formal_argument);
   API_FUNCTION(kllvm_init);
   API_FUNCTION(kllvm_free_all_memory);
+  API_FUNCTION(kllvm_mutable_bytes_enabled);
 
   return api;
 }

test/c/Inputs/api.h

@@ -52,6 +52,7 @@ struct kllvm_c_api {
   void (*kore_symbol_add_formal_argument)(kore_symbol *, kore_sort const *);
   void (*kllvm_init)(void);
   void (*kllvm_free_all_memory)(void);
+  bool (*kllvm_mutable_bytes_enabled)(void);
 };
 
 struct kllvm_c_api load_c_api(char const *);