Merge remote-tracking branch 'origin/develop'

Author: rv-auditor

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{}()]