Version header for proof hints (#885)

fixes: #883 --------- Co-authored-by: rv-jenkins <[email protected]>
runtimeverification · Nov 16, 2023 · b5ccb96 · b5ccb96
1 parent 39e5557
commit b5ccb96
Show file tree

Hide file tree

Showing 3 changed files with 20 additions and 1 deletion.
diff --git a/docs/proof-trace.md b/docs/proof-trace.md
@@ -21,7 +21,9 @@ have rendered this unnecessary, but the change hasn't been implemented yet.
 
 Here is a BNF styled description of the format:
 ```
-proof_trace ::= event*
+proof_trace ::= header event*
+
+header      ::= "HINT" <4-byte version number>
 
 event       ::= hook
               | function

diff --git a/runtime/main/main.ll b/runtime/main/main.ll
@@ -12,6 +12,8 @@ declare void @finish_rewriting(%block*, i1) #0
 
 declare void @initStaticObjects()
 
+declare void @printProofHintHeader(i8*)
+
 @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"
@@ -91,6 +93,12 @@ entry:
 
   call void @initStaticObjects()
 
+  %proof_output = load i1, i1* @proof_output
+  br i1 %proof_output, label %if, label %else
+if:
+  call void @printProofHintHeader(i8* %output_str)
+  br label %else
+else:
   %ret = call %block* @parseConfiguration(i8* %filename)
   %result = call %block* @take_steps(i64 %depth, %block* %ret)
   call void @finish_rewriting(%block* %result, i1 0)

diff --git a/runtime/util/util.cpp b/runtime/util/util.cpp
@@ -28,4 +28,13 @@ block *constructKItemInj(void *subject, const char *sort, bool raw_value) {
   auto args = std::vector<void *>{add_indirection ? (void *)&subject : subject};
   return static_cast<block *>(constructCompositePattern(tag, args));
 }
+
+void printProofHintHeader(char *output_file) {
+  unsigned int version = 1;
+  FILE *file = fopen(output_file, "a");
+  fprintf(file, "HINT");
+  fwrite(&version, sizeof(version), 1, file);
+  fflush(file);
+  fclose(file);
+}
 }