Remove sentinel for end of KORE terms in the proof hint format (#1076)

This PR removes the sentinel at the end of a KORE terms as it would
appear in the proof hint trace. We do not need this sentinel to properly
parse the trace because the KORE term binary format includes length
information.

The hints version has been bumped to 11 and the relevant tests have been
updated.

Author: theo25

docs/proof-trace.md

@@ -26,7 +26,6 @@ static_assert(word(0xAA) == 0xAAAAAAAAAAAAAAAA);
 } // namespace detail
 
 constexpr uint64_t config_sentinel = detail::word(0xFF);
-constexpr uint64_t kore_end_sentinel = detail::word(0xCC);
 constexpr uint64_t function_event_sentinel = detail::word(0xDD);
 constexpr uint64_t function_end_sentinel = detail::word(0x11);
 constexpr uint64_t hook_event_sentinel = detail::word(0xAA);
@@ -274,7 +273,7 @@ class llvm_rewrite_trace {
 
 class proof_trace_parser {
 public:
-  static constexpr uint32_t expected_version = 10U;
+  static constexpr uint32_t expected_version = 11U;
 
 private:
   bool verbose_;
@@ -332,7 +331,7 @@ class proof_trace_parser {
 
     event->add_substitution(name, kore_term, pattern_len);
 
-    return buffer.check_word(kore_end_sentinel);
+    return true;
   }
 
   sptr<llvm_hook_event> parse_hook(proof_trace_buffer &buffer) {
@@ -422,10 +421,6 @@ class proof_trace_parser {
       return nullptr;
     }
 
-    if (!buffer.check_word(kore_end_sentinel)) {
-      return nullptr;
-    }
-
     return kore_term;
   }
 

include/kllvm/binary/ProofTraceParser.h

@@ -255,7 +255,6 @@ llvm::BasicBlock *proof_event::rewrite_event_pre(
 
     emit_write_string(outputFile, key.str(), true_block);
     emit_serialize_term(*sort, outputFile, val, true_block);
-    emit_write_uint64(outputFile, detail::word(0xCC), true_block);
   }
 
   llvm::BranchInst::Create(merge_block, true_block);
@@ -277,7 +276,6 @@ llvm::BasicBlock *proof_event::rewrite_event_post(
 
   emit_write_uint64(output_file, detail::word(0xFF), true_block);
   emit_serialize_term(*return_sort, output_file, return_value, true_block);
-  emit_write_uint64(output_file, detail::word(0xCC), true_block);
 
   llvm::BranchInst::Create(merge_block, true_block);
   return merge_block;
@@ -353,7 +351,6 @@ llvm::BasicBlock *proof_event::side_condition_event_pre(
 
     emit_write_string(outputFile, var_name, true_block);
     emit_serialize_term(*sort, outputFile, val, true_block);
-    emit_write_uint64(outputFile, detail::word(0xCC), true_block);
   }
 
   llvm::BranchInst::Create(merge_block, true_block);

lib/codegen/ProofEvent.cpp

@@ -52,7 +52,6 @@ if:
   %output_file = load i8*, i8** @output_file
   call void @write_uint64_to_file(i8* %output_file, i64 18446744073709551615)
   call void @serialize_configuration_to_file_v2(i8* %output_file, %block* %subject)
-  call void @write_uint64_to_file(i8* %output_file, i64 14757395258967641292)
   br label %merge
 merge:
   store i64 %depth, i64* @depth

runtime/take_steps.ll

@@ -48,7 +48,6 @@ int32_t get_exit_code(block *);
   } else if (!error && !proof_hint_instrumentation_slow) {
     write_uint64_to_file(output_file, 0xFFFFFFFFFFFFFFFF);
     serialize_configuration_to_file_v2(output_file, subject);
-    write_uint64_to_file(output_file, 0xCCCCCCCCCCCCCCCC);
   }
 
   auto exit_code = error ? 113 : get_exit_code(subject);

runtime/util/finish_rewriting.cpp

@@ -35,7 +35,7 @@ block *construct_raw_term(void *subject, char const *sort, bool raw_value) {
 }
 
 void print_proof_hint_header(FILE *file) {
-  uint32_t version = 10;
+  uint32_t version = 11;
   fmt::print(file, "HINT");
   fwrite(&version, sizeof(version), 1, file);
 }

runtime/util/util.cpp

@@ -1,4 +1,4 @@
-version: 10
+version: 11
 hook: MAP.element Lbl'UndsPipe'-'-GT-Unds'{} ()
   function: Lbl'UndsPipe'-'-GT-Unds'{} ()
   arg: kore[\dv{SortKConfigVar{}}("$PGM")]

test/output/add-rewrite/input.proof.out.diff

@@ -1,4 +1,4 @@
-version: 10
+version: 11
 hook: MAP.element Lbl'UndsPipe'-'-GT-Unds'{} ()
   function: Lbl'UndsPipe'-'-GT-Unds'{} ()
   arg: kore[\dv{SortKConfigVar{}}("$PGM")]

test/output/arith/add.proof.out.diff

@@ -1,4 +1,4 @@
-version: 10
+version: 11
 hook: MAP.element Lbl'UndsPipe'-'-GT-Unds'{} ()
   function: Lbl'UndsPipe'-'-GT-Unds'{} ()
   arg: kore[\dv{SortKConfigVar{}}("$PGM")]

test/output/arith/well.proof.out.diff

@@ -1,4 +1,4 @@
-version: 10
+version: 11
 function: Lbl'UndsPlus'left'UndsUnds'ASSOC-FUNCTION-SYNTAX'Unds'Foo'Unds'Foo'Unds'Foo{} ()
 rule: 103 2
   Var'Unds'X = kore[Lbla'Unds'ASSOC-FUNCTION-SYNTAX'Unds'Foo{}()]