Omitting intemedaite configuration events in the proof trace (#1025)

This PR disables the generation of intermediate configuration events in
the proof trace by default. It is a followup of #1020 and aims to
further improve the performance of generating hints. Similarly to #1020,
we allow the user to get the old behavior of emitting every intermediate
configuration event by passing the `--proof-hint-instrumentation-slow`
flag to `llvm-kompile`.

---------

Co-authored-by: Dwight Guth <[email protected]>

bin/llvm-kompile

@@ -35,7 +35,8 @@ Options:
   -fno-omit-frame-pointer           Keep the frame pointer in compiled code for debugging purposes.
   --proof-hint-instrumentation      Enable instrumentation for generation of proof hints.
   --proof-hint-instrumentation-slow Enable instrumentation for generation of proof hints that
-                                    contain function argument KORE terms as part of the trace.
+                                    contains debugging events that are not strictly required.
+                                    Significantly slower than the less verbose version.
   --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.

docs/proof-trace.md

@@ -1,16 +1,21 @@
 # Proof Trace Format
 
 This document describes the format for the binary proof trace that gets emitted
-when the `--proof-output` flag gets passed to the interpreter. Note that this trace
+when the `--proof-output` flag gets passed to the interpreter. In order for the trace
+to be emitted, an appropriate instrumentation flag should have been passed to `llvm-kompile`.
+We currently offer two modes of instrumentation: the default one is enabled with the flag
+`--proof-hint-instrumentation`, while a slower one that generates a longer trace is enabled with
+the flag `--proof-hint-instrumentation-slow`. Note that this trace
 format is in its early stages and will probably change quite a bit as development on it
 continues.
 
 ## Overview
 
 The information presented by the trace starts with the initial configuration of the execution,
-followed by a sequence of rewrite steps consisting of which rule applied, the variable substitutions
-for that rule, and the resulting configuration after the rewrite, and then finally the configuration
-at the end of the execution.
+followed by a sequence of rewrite steps consisting of which rule applied and the variable substitutions
+for that rule, and finally the configuration at the end of the execution. If slow instrumentation
+has been enabled, the trace additionally contains the intermediate configurations after each rewrite
+event, as well as the kore terms that are passed as arguments in function events.
 
 The format of the kore terms themselves are in binary format, and in the proof trace we delimit
 them with 64-bit sentinel values of 0xffffffffffffffff at the beginning and 0xcccccccccccccccc
@@ -21,7 +26,7 @@ have rendered this unnecessary, but the change hasn't been implemented yet.
 
 Here is a BNF styled description of the format:
 ```
-proof_trace ::= header event*
+proof_trace ::= header event* // only starting and final config events in normal mode
 
 header            ::= "HINT" <4-byte version number>
 
@@ -39,7 +44,7 @@ argument          ::= hook
 
 name              ::= string
 location          ::= string
-function          ::= WORD(0xDD) name location arg* WORD(0x11)
+function          ::= WORD(0xDD) name location arg* WORD(0x11) // the arg list is ommited in normal mode
 
 hook              ::= WORD(0xAA) name location arg* WORD(0xBB) kore_term
 

include/kllvm/binary/ProofTraceParser.h

@@ -260,7 +260,7 @@ class llvm_rewrite_trace {
 
 class proof_trace_parser {
 public:
-  static constexpr uint32_t expected_version = 7U;
+  static constexpr uint32_t expected_version = 8U;
 
 private:
   bool verbose_;

include/kllvm/codegen/Metadata.h

@@ -15,6 +15,8 @@ void add_mutable_bytes_flag(llvm::Module &mod, bool enabled, bool debug);
 
 void add_safe_partial_flag(llvm::Module &mod, bool enabled, bool debug);
 
+void add_proof_hint_instrumentation_slow_flag(
+    llvm::Module &mod, bool enabled, bool debug);
 } // namespace kllvm
 
 #endif

lib/codegen/Metadata.cpp

@@ -13,6 +13,7 @@ namespace {
 std::string kompiled_dir = "kompiled_directory";
 std::string strict_bytes = "enable_mutable_bytes";
 std::string safe_partial = "safe_partial";
+std::string proof_hint_instrumentation_slow = "proof_hint_instrumentation_slow";
 
 void add_boolean_flag(
     llvm::Module &mod, std::string const &name, bool enabled, bool debug) {
@@ -61,4 +62,9 @@ void add_safe_partial_flag(llvm::Module &mod, bool enabled, bool debug) {
   add_boolean_flag(mod, safe_partial, enabled, debug);
 }
 
+void add_proof_hint_instrumentation_slow_flag(
+    llvm::Module &mod, bool enabled, bool debug) {
+  add_boolean_flag(mod, proof_hint_instrumentation_slow, enabled, debug);
+}
+
 } // namespace kllvm

lib/codegen/ProofEvent.cpp

@@ -288,7 +288,7 @@ llvm::BasicBlock *proof_event::rewrite_event_pre(
 llvm::BasicBlock *proof_event::rewrite_event_post(
     kore_axiom_declaration *axiom, llvm::Value *return_value,
     llvm::BasicBlock *current_block) {
-  if (!proof_hint_instrumentation) {
+  if (!proof_hint_instrumentation_slow) {
     return current_block;
   }
 

runtime/util/finish_rewriting.cpp

@@ -13,6 +13,7 @@ bool proof_output = false;
 
 extern int64_t steps;
 extern bool safe_partial;
+extern bool proof_hint_instrumentation_slow;
 
 int32_t get_exit_code(block *);
 
@@ -44,6 +45,10 @@ int32_t get_exit_code(block *);
     } else {
       print_configuration(output_file, subject);
     }
+  } else if (!error && !proof_hint_instrumentation_slow) {
+    write_uint64_to_file(output_file, 0xFFFFFFFFFFFFFFFF);
+    serialize_configuration_to_file(output_file, subject, true, false);
+    write_uint64_to_file(output_file, 0xCCCCCCCCCCCCCCCC);
   }
 
   auto exit_code = error ? 113 : get_exit_code(subject);

runtime/util/util.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 = 7;
+  uint32_t version = 8;
   fmt::print(file, "HINT");
   fwrite(&version, sizeof(version), 1, file);
 }