Shared memory writer for proof hints (#1122)

This PR adds a subclass of the abstract `proof_trace_writer` for
outputting hints into a ringbuffer that lives in shared memory. This
output method is intended to be used with the shared memory option of
the `kore-proof-trace` parser to communicate hints through shared memory
instead of through a file.

Since we now can test the shared memory based proof
generation/consumption loop, we also do not include the helper
`kore-proof-trace-shm-writer` tool in the installation.

include/kllvm/binary/serializer.h

@@ -2,6 +2,7 @@
 #define AST_SERIALIZER_H
 
 #include <kllvm/ast/AST.h>
+#include <kllvm/binary/ringbuffer.h>
 #include <kllvm/binary/version.h>
 
 #include <array>
@@ -160,6 +161,8 @@ class proof_trace_writer {
     write(&n, 1);
   }
 
+  virtual void write_eof() = 0;
+
   void write_bool(bool b) { write(&b, sizeof(bool)); }
   void write_uint32(uint32_t i) { write(&i, sizeof(uint32_t)); }
   void write_uint64(uint64_t i) { write(&i, sizeof(uint64_t)); }
@@ -172,9 +175,42 @@ class proof_trace_file_writer : public proof_trace_writer {
 public:
   proof_trace_file_writer(FILE *file)
       : file_(file) { }
+
+  void write(void const *ptr, size_t len) override;
+  void write_string(char const *str, size_t len) override;
+  void write_string(char const *str) override;
+  void write_eof() override { }
+};
+
+class proof_trace_ringbuffer_writer : public proof_trace_writer {
+private:
+  shm_ringbuffer *shm_buffer_;
+  sem_t *data_avail_;
+  sem_t *space_avail_;
+
+  void write(uint8_t const *ptr, size_t len = 1);
+
+public:
+  proof_trace_ringbuffer_writer(
+      void *shm_object, sem_t *data_avail, sem_t *space_avail)
+      : shm_buffer_(reinterpret_cast<shm_ringbuffer *>(shm_object))
+      , data_avail_(data_avail)
+      , space_avail_(space_avail) { }
+
+  ~proof_trace_ringbuffer_writer() override { shm_buffer_->~shm_ringbuffer(); }
+
+  proof_trace_ringbuffer_writer(proof_trace_ringbuffer_writer const &) = delete;
+  proof_trace_ringbuffer_writer(proof_trace_ringbuffer_writer &&) = delete;
+  proof_trace_ringbuffer_writer &
+  operator=(proof_trace_ringbuffer_writer const &)
+      = delete;
+  proof_trace_ringbuffer_writer &operator=(proof_trace_ringbuffer_writer &&)
+      = delete;
+
   void write(void const *ptr, size_t len) override;
   void write_string(char const *str, size_t len) override;
   void write_string(char const *str) override;
+  void write_eof() override;
 };
 
 } // namespace kllvm

lib/binary/serializer.cpp

@@ -222,4 +222,31 @@ void proof_trace_file_writer::write_string(char const *str) {
   fputs(str, file_);
 }
 
+void proof_trace_ringbuffer_writer::write(uint8_t const *ptr, size_t len) {
+  for (size_t i = 0; i < len; i++) {
+    sem_wait(space_avail_);
+    shm_buffer_->put(&ptr[i]);
+    sem_post(data_avail_);
+  }
+}
+
+void proof_trace_ringbuffer_writer::write(void const *ptr, size_t len) {
+  auto const *data = reinterpret_cast<uint8_t const *>(ptr);
+  write(data, len);
+}
+
+void proof_trace_ringbuffer_writer::write_string(char const *str, size_t len) {
+  auto const *data = reinterpret_cast<uint8_t const *>(str);
+  write(data, len);
+}
+
+void proof_trace_ringbuffer_writer::write_string(char const *str) {
+  auto const *data = reinterpret_cast<uint8_t const *>(str);
+  write(data, strlen(str));
+}
+
+void proof_trace_ringbuffer_writer::write_eof() {
+  shm_buffer_->put_eof();
+}
+
 } // namespace kllvm

runtime/main/main.ll

@@ -19,11 +19,13 @@ declare void @print_proof_hint_header(ptr)
 @statistics.flag = private constant [13 x i8] c"--statistics\00"
 @binary_out.flag = private constant [16 x i8] c"--binary-output\00"
 @proof_out.flag = private constant [15 x i8] c"--proof-output\00"
+@use_shm.flag = private constant [20 x i8] c"--use-shared-memory\00"
 
 @proof_writer = external global ptr
 @statistics = external global i1
 @binary_output = external global i1
 @proof_output = external global i1
+@use_shm = external global i1
 
 declare i32 @strcmp(ptr %a, ptr %b)
 
@@ -63,10 +65,19 @@ binary.set:
 proof.body:
   %proof.cmp = call i32 @strcmp(ptr %arg, ptr getelementptr inbounds ([15 x i8], ptr @proof_out.flag, i64 0, i64 0))
   %proof.eq = icmp eq i32 %proof.cmp, 0
-  br i1 %proof.eq, label %proof.set, label %body.tail
+  br i1 %proof.eq, label %proof.set, label %shm.body
 
 proof.set:
   store i1 1, ptr @proof_output
+  br label %shm.body
+
+shm.body:
+  %shm.cmp = call i32 @strcmp(ptr %arg, ptr getelementptr inbounds ([20 x i8], ptr @use_shm.flag, i64 0, i64 0))
+  %shm.eq = icmp eq i32 %shm.cmp, 0
+  br i1 %shm.eq, label %shm.set, label %body.tail
+
+shm.set:
+  store i1 1, ptr @use_shm
   br label %body.tail
 
 body.tail:

runtime/util/finish_rewriting.cpp

@@ -1,24 +1,77 @@
+#include <kllvm/binary/serializer.h>
+
 #include <runtime/header.h>
 
 #include <cstdint>
+#include <fcntl.h>
 #include <iostream>
 #include <memory>
+#include <sys/mman.h>
 
 extern "C" {
 
 FILE *output_file = nullptr;
-kllvm::proof_trace_writer *proof_writer = nullptr;
+void *proof_writer = nullptr;
 bool statistics = false;
 bool binary_output = false;
 bool proof_output = false;
+bool use_shm = false;
 
 extern int64_t steps;
 extern bool safe_partial;
 extern bool proof_hint_instrumentation_slow;
 
 int32_t get_exit_code(block *);
 
+#define ERR_EXIT(msg)                                                          \
+  do {                                                                         \
+    perror(msg);                                                               \
+    exit(1);                                                                   \
+  } while (0)
+
+static void set_up_shm_writer(char const *output_filename) {
+  // Open existing shared memory object
+  int fd = shm_open(output_filename, O_RDWR, 0);
+  if (fd == -1) {
+    ERR_EXIT("shm_open writer");
+  }
+
+  // Map the object into the caller's address space
+  size_t shm_size = sizeof(kllvm::shm_ringbuffer);
+  void *shm_object
+      = mmap(nullptr, shm_size, PROT_READ | PROT_WRITE, MAP_SHARED, fd, 0);
+  if (shm_object == MAP_FAILED) {
+    ERR_EXIT("mmap writer");
+  }
+
+  // MacOS has deprecated unnamed semaphores, so we need to use named ones
+  std::string base_name(output_filename);
+  std::string data_avail_sem_name = base_name + ".d";
+  std::string space_avail_sem_name = base_name + ".s";
+
+  // Open existing semaphores
+  // NOLINTNEXTLINE(*-pro-type-vararg)
+  sem_t *data_avail = sem_open(data_avail_sem_name.c_str(), 0);
+  if (data_avail == SEM_FAILED) {
+    ERR_EXIT("sem_init data_avail writer");
+  }
+  // NOLINTNEXTLINE(*-pro-type-vararg)
+  sem_t *space_avail = sem_open(space_avail_sem_name.c_str(), 0);
+  if (space_avail == SEM_FAILED) {
+    ERR_EXIT("sem_init space_avail writer");
+  }
+
+  // Create the proof_trace_ringbuffer_writer object
+  proof_writer = new kllvm::proof_trace_ringbuffer_writer(
+      shm_object, data_avail, space_avail);
+}
+
 void init_outputs(char const *output_filename) {
+  if (proof_output && use_shm) {
+    set_up_shm_writer(output_filename);
+    return;
+  }
+
   output_file = fopen(output_filename, "a");
   if (proof_output) {
     proof_writer = new kllvm::proof_trace_file_writer(output_file);
@@ -34,17 +87,19 @@ void init_outputs(char const *output_filename) {
       = std::unique_ptr<FILE, decltype(&fclose)>(output_file, fclose);
 
   // Similar for deletinging the proof_output_buffer data structure
-  [[maybe_unused]] auto deleter
-      = std::unique_ptr<kllvm::proof_trace_writer>(proof_writer);
+  auto *w = static_cast<kllvm::proof_trace_writer *>(proof_writer);
+  [[maybe_unused]] auto deleter = std::unique_ptr<kllvm::proof_trace_writer>(w);
 
   if (error && safe_partial) {
     throw std::runtime_error(
         "Attempted to evaluate partial function at an undefined input");
   }
 
   if (!output_file) {
-    throw std::runtime_error(
-        "Called finish_rewriting with no output file specified");
+    if (!proof_output || !use_shm) {
+      throw std::runtime_error(
+          "Called finish_rewriting with no output file specified");
+    }
   }
 
   if (statistics) {
@@ -58,11 +113,16 @@ void init_outputs(char const *output_filename) {
       print_configuration(output_file, subject);
     }
   } else if (!error && !proof_hint_instrumentation_slow) {
-    write_uint64_to_proof_trace(proof_writer, 0xFFFFFFFFFFFFFFFF);
+    w->write_uint64(0xFFFFFFFFFFFFFFFF);
     serialize_configuration_to_proof_writer(proof_writer, subject);
   }
 
   auto exit_code = error ? 113 : get_exit_code(subject);
+
+  if (proof_output) {
+    w->write_eof();
+  }
+
   std::exit(exit_code);
 }
 }

test/defn/imp-sum-slow.kore

@@ -1,5 +1,6 @@
 // RUN: %proof-slow-interpreter
 // RUN: %check-proof-out
+// RUN: %check-proof-shm-out
 [topCellInitializer{}(LblinitGeneratedTopCell{}()), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/llvm-backend/src/main/native/llvm-backend/test/defn/k-files/imp.md)")]
 
 module BASIC-K

test/defn/imp-sum.kore

@@ -1,5 +1,6 @@
 // RUN: %proof-interpreter
 // RUN: %check-proof-out
+// RUN: %check-proof-shm-out
 [topCellInitializer{}(LblinitGeneratedTopCell{}()), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/llvm-backend/src/main/native/llvm-backend/test/defn/k-files/imp.md)")]
 
 module BASIC-K

test/defn/imp.kore

@@ -2,6 +2,7 @@
 // RUN: %check-grep
 // RUN: %proof-interpreter
 // RUN: %check-proof-out
+// RUN: %check-proof-shm-out
 [topCellInitializer{}(LblinitGeneratedTopCell{}()), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/llvm-backend/src/main/native/llvm-backend/test/defn/k-files/imp.md)")]
 
 module BASIC-K

test/defn/kool-static.kore

@@ -2,6 +2,7 @@
 // RUN: %check-diff
 // RUN: %proof-interpreter
 // RUN: %check-proof-out
+// RUN: %check-proof-shm-out
 [topCellInitializer{}(LblinitGeneratedTopCell{}()), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework-5.0.0/k-distribution/pl-tutorial/2_languages/2_kool/2_typed/2_static/kool-typed-static.md)")]
 
 module BASIC-K

test/lit.cfg.py

@@ -167,10 +167,14 @@ def one_line(s):
             echo "kore-proof-trace error while parsing proof hint trace with expanded kore terms and streaming parser"
             exit 1
         fi
+    ''')),
+
+    ('%check-proof-shm-out', one_line('''
+        %kore-rich-header %s > %t.header.bin
         %kore-proof-trace --shared-memory --verbose --expand-terms %t.header.bin %test-shm-buffer | diff - %test-proof-diff-out &
         reader_pid="$!"
         sleep 1
-        %kore-proof-trace-shm-writer %t.out.bin %test-shm-buffer
+        %run-proof-shm-out
         wait $reader_pid
         result="$?"
         if [ "$result" -ne 0 ]; then
@@ -196,11 +200,9 @@ def one_line(s):
 
     ('%check-dir-proof-out', one_line('''
         %kore-rich-header %s > %t.header.bin
-        count=0
         for out in %test-dir-out/*.proof.out.diff; do
             in=%test-dir-in/`basename $out .proof.out.diff`.in
             hint=%t.`basename $out .proof.out.diff`.hint
-            shmbuf=%test-shm-buffer.$count
             rm -f $hint
             %t.interpreter $in -1 $hint --proof-output
             %kore-proof-trace --verbose --expand-terms %t.header.bin $hint | diff - $out
@@ -215,10 +217,19 @@ def one_line(s):
                 echo "kore-proof-trace error while parsing proof hint trace with expanded kore terms and streaming parser"
                 exit 1
             fi
+        done
+    ''')),
+
+    ('%check-dir-proof-shm-out', one_line('''
+        %kore-rich-header %s > %t.header.bin
+        count=0
+        for out in %test-dir-out/*.proof.out.diff; do
+            in=%test-dir-in/`basename $out .proof.out.diff`.in
+            shmbuf=%test-shm-buffer.$count
             %kore-proof-trace --shared-memory --verbose --expand-terms %t.header.bin $shmbuf | diff - $out &
             reader_pid="$!"
             sleep 1
-            %kore-proof-trace-shm-writer $hint $shmbuf
+            %t.interpreter $in -1 $shmbuf --proof-output --use-shared-memory
             wait $reader_pid
             result="$?"
             if [ "$result" -ne 0 ]; then
@@ -232,6 +243,7 @@ def one_line(s):
     ('%run-binary-out', 'rm -f %t.out.bin && %t.interpreter %test-input -1 %t.out.bin --binary-output'),
     ('%run-binary', 'rm -f %t.bin && %convert-input && %t.interpreter %t.bin -1 /dev/stdout'),
     ('%run-proof-out', 'rm -f %t.out.bin && %t.interpreter %test-input -1 %t.out.bin --proof-output'),
+    ('%run-proof-shm-out', '%t.interpreter %test-input -1 %test-shm-buffer --proof-output --use-shared-memory'),
     ('%run', '%t.interpreter %test-input -1 /dev/stdout'),
 
     ('%kprint-check', 'kprint %S %s true | diff - %s.out'),

test/proof/add-rewrite.kore

@@ -1,5 +1,6 @@
 // RUN: %proof-interpreter
 // RUN: %check-dir-proof-out
+// RUN: %check-dir-proof-shm-out
 // RUN: %check-proof-debug-out
 [topCellInitializer{}(LblinitGeneratedTopCell{}()), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/proof-checker/generation/k-benchmarks/add-rewrite/add-rewrite.k)")]
 

test/proof/arith.kore

@@ -1,5 +1,6 @@
 // RUN: %proof-interpreter
 // RUN: %check-dir-proof-out
+// RUN: %check-dir-proof-shm-out
 [topCellInitializer{}(LblinitGeneratedTopCell{}()), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/proof-checker/generation/k-benchmarks/arith/arith.k)")]
 
 module BASIC-K

test/proof/assoc-function.kore

@@ -1,5 +1,6 @@
 // RUN: %proof-interpreter
 // RUN: %check-dir-proof-out
+// RUN: %check-dir-proof-shm-out
 [topCellInitializer{}(LblinitGeneratedTopCell{}()), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/proof-checker/generation/k-benchmarks/assoc-function/assoc-function.k)")]
 
 module BASIC-K

test/proof/builtin-functions.kore

@@ -1,5 +1,6 @@
 // RUN: %proof-interpreter
 // RUN: %check-dir-proof-out
+// RUN: %check-dir-proof-shm-out
 [topCellInitializer{}(LblinitGeneratedTopCell{}()), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/proof-checker/generation/k-benchmarks/builtin-functions/builtin-functions.k)")]
 
 module BASIC-K

test/proof/builtin-hook-events.kore

@@ -1,5 +1,6 @@
 // RUN: %proof-interpreter
 // RUN: %check-dir-proof-out
+// RUN: %check-dir-proof-shm-out
 [topCellInitializer{}(LblinitGeneratedTopCell{}()), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/proof-checker/generation/k-benchmarks/builtin-hook-events/builtin-hook-events.k)")]
 
 module BASIC-K

test/proof/builtin-int.kore

@@ -1,5 +1,6 @@
 // RUN: %proof-interpreter
 // RUN: %check-dir-proof-out
+// RUN: %check-dir-proof-shm-out
 [topCellInitializer{}(LblinitGeneratedTopCell{}()), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/proof-checker/generation/k-benchmarks/builtin-int/builtin-int.k)")]
 
 module BASIC-K

test/proof/builtin-io.kore

@@ -1,5 +1,6 @@
 // RUN: %proof-interpreter
 // RUN: %check-dir-proof-out
+// RUN: %check-dir-proof-shm-out
 [topCellInitializer{}(LblinitGeneratedTopCell{}()), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/proof-checker/generation/k-benchmarks/builtin-io/builtin-io.k)")]
 
 module BASIC-K

test/proof/builtin-json.kore

@@ -1,5 +1,6 @@
 // RUN: %proof-interpreter
 // RUN: %check-dir-proof-out
+// RUN: %check-dir-proof-shm-out
 [topCellInitializer{}(LblinitGeneratedTopCell{}()), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/proof-checker/generation/k-benchmarks/builtin-json/builtin-json.k)")]
 
 module BASIC-K

test/proof/cast.kore

@@ -1,5 +1,6 @@
 // RUN: %proof-interpreter
 // RUN: %check-dir-proof-out
+// RUN: %check-dir-proof-shm-out
 [topCellInitializer{}(LblinitGeneratedTopCell{}()), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/proof-checker/generation/k-benchmarks/cast/cast.k)")]
 
 module BASIC-K