Move rewrite event emission (#877)

This PR is a reworking of the changes initially made by @gtrepta in
#862, to include the cleaned-up proof infrastructure in #876.

The changes here are pretty minimal; we need to split the "rewrite"
event into a pre and post part so that the arity / ordinal and resulting
configuration can be emitted separately. Other than that, it's just a
question of reusing some of the boilerplate in #862 that assembles the
substitution information in the event.

~~There is one major issue with the change here, which @gtrepta also
identified in his initial version of this change. We can only emit
resulting configurations for top-level rewrites (that is, we cannot
print the resulting _term_ from calling a function). Doing so breaks TCO
for the generated interpreter badly enough that some backend tests
crash; I have not dug into this in detail as I'm reasonably sure that's
the reason things break.~~
* @nishantjr confirms that we can safely omit the result of function
calls from the trace.

## Outstanding Issues

I am working my way through the example below to ensure that the format
being generated is precisely what we expect to see from the
documentation. The issues I have identified are as follows:
* [x] Duplicated KORE comments below are caused by function events not
being bracketed as rewrites and hooks are; we need to pull the header
out to the front, allocate args, then do the existing event.
* [x] We need to handle binary KORE delimitation more consistently; at
the moment it's wavy whether we emit header / footer or not. Should
probably standardise on using the 1.2.0 self-limiting format.

## Worked Example

Similarly to #862, I have generated a trace for the program `foo(0)` in
the following definition:
```k
module TEST
  imports INT

  syntax Int ::= "inc" Int [function, total]
  rule inc I => I +Int 1

  syntax Foo ::= foo(Int) | bar(Int)
  rule foo(I) => bar(inc I)
endmodule
```

The trace looks like:
```
hook: MAP.element
  function: Lbl'UndsPipe'-'-GT-Unds'{} (0)
    arg: kore[60]
    arg: kore[109]
hook result: kore[207]
hook: MAP.unit
  function: Lbl'Stop'Map{} (0)
hook result: kore[51]
hook: MAP.concat
  function: Lbl'Unds'Map'Unds'{} (0)
    arg: kore[51]
    arg: kore[207]
hook result: kore[207]
function: LblinitGeneratedTopCell{} (0)
  arg: kore[207]
rule: 162 1
  VarInit = kore[207]
function: LblinitKCell{} (0:0)
  arg: kore[207]
rule: 163 1
  VarInit = kore[207]
function: Lblproject'Coln'KItem{} (0:0:0)
  hook: MAP.lookup
    function: LblMap'Coln'lookup{} (0:0:0:0:0)
      arg: kore[207]
      arg: kore[60]
  hook result: kore[109]
  arg: kore[129]
rule: 207 1
  VarK = kore[109]
function: LblinitGeneratedCounterCell{} (0:1)
rule: 161 0
config: kore[237]
rule: 126 3
  Var'Unds'DotVar0 = kore[61]
  VarI = kore[50]
  Var'Unds'DotVar1 = kore[10]
function: Lblinc'UndsUnds'TEST'Unds'Int'Unds'Int{} (0:0:0:0:0:0)
  arg: kore[50]
rule: 160 1
  VarI = kore[50]
hook: INT.add
  function: Lbl'UndsPlus'Int'Unds'{} (0)
    arg: kore[50]
    arg: kore[50]
hook result: kore[50]
config: kore[237]
```

And was generated with the following (really horrible, quick and dirty)
Python recogniser:
<details><summary>Recogniser</summary>

```python
#!/usr/bin/env python3

import sys
import struct

def load(fn):
    with open(fn, 'rb') as f:
        return f.read()

def word(byte):
    return byte * 8

class Parser:
    def __init__(self, data):
        self.input = data
        self.depth = 0

    def print(self, *args):
        print(f'{"  " * self.depth}', end='')
        print(*args)

    def peek(self, cst):
        return self.input[:len(cst)] == cst

    def eof(self):
        return len(self.input) == 0

    def skip(self, n):
        self.input = self.input[n:]

    def read_constant(self, cst):
        if self.input[:len(cst)] != cst:
            print(self.input[:40])
            assert False
        self.input = self.input[len(cst):]

    def read_word(self, byte):
        assert len(byte) == 1
        self.read_constant(byte * 8)

    def read_until(self, constant):
        index = self.input.find(constant)
        ret = self.input[:index]
        self.input = self.input[index:]
        return ret
    
    def read_string(self):
        data = self.read_until(b'\x00')
        self.read_constant(b'\x00')
        return str(data, 'ascii')

    def read_uint64(self):
        index = 8
        raw = self.input[:index]
        self.input = self.input[index:]
        little_endian_long_long = '<Q'
        return struct.unpack(little_endian_long_long, raw)[0]

    def read_arg(self):
        self.depth += 1
        if self.peek(b'\x7F'):
            l = self.read_kore()
            self.print(f'arg: kore[{l}]')
            self.depth -= 1
            return True
        elif self.peek(word(b'\xDD')):
            self.read_function()
            self.depth -= 1
            return True
        elif self.peek(word(b'\xAA')):
            self.read_hook()
            self.depth -= 1
            return True
        elif self.peek(word(b'\x11')) or self.peek(word(b'\xBB')):
            self.depth -= 1
            return False
        else:
            self.read_rule()
            self.depth -= 1
            return True

    def read_hook(self):
        self.read_word(b'\xAA')
        name = self.read_string()
        self.print(f'hook: {name}')
        while True:
            if not self.read_arg():
                break
        self.read_word(b'\xBB')
        result = self.read_kore()
        self.print(f'hook result: kore[{result}]')

    def read_function(self):
        self.read_word(b'\xDD')
        label = self.read_string()
        loc = self.read_string()
        self.print(f'function: {label} ({loc})')
        while True:
            if not self.read_arg():
                break
        self.read_word(b'\x11')

    def read_kore(self):
        self.read_constant(b'\x7FKORE')
        self.skip(6)
        pattern_len = self.read_uint64()
        self.skip(pattern_len)
        return pattern_len

    def read_rule(self):
        ordinal = self.read_uint64()
        arity = self.read_uint64()
        self.print(f'rule: {ordinal} {arity}')
        for i in range(arity):
            self.read_variable()

    def read_variable(self):
        name = self.read_string()
        kore_len = self.read_kore()
        self.print(f'  {name} = kore[{kore_len}]')
        self.read_word(b'\xCC')

    def read_config(self):
        self.read_word(b'\xFF')
        l = self.read_kore()
        self.print(f'config: kore[{l}]')
        self.read_word(b'\xCC')

    def read_trace(self):
        while not self.eof():
            if self.peek(word(b'\xAA')):
                self.read_hook()
            elif self.peek(word(b'\xDD')):
                self.read_function()
            elif self.peek(word(b'\xFF')):
                self.read_config()
            else:
                self.read_rule()
            
if __name__ == '__main__':
    data = load(sys.argv[1])
    parser = Parser(data)
    parser.read_trace()
```
</details>

I have verified by hand that this recogniser accepts all the proof
traces from the proof generation repo's master branch, if they are
regenerated with the LLVM backend pointed at this PR (`kup install k
--override llvm-backend hint_emitPlace_2`).

Author: Baltoli

Diff for: docs/proof-trace.md

@@ -19,38 +19,42 @@ have rendered this unnecessary, but the change hasn't been implemented yet.
 
 ## Grammar
 
-Here is a BNF styled description of the format
-
+Here is a BNF styled description of the format:
 ```
-delimited_serial_kore := 0xffffffffffffffff serialized_term 0xcccccccccccccccc
-
-null_terminated_name := <c-style null terminated string>
-relative_position := [0-9]+(:[0-9]+)* 0x00
-
-function_event := 0xdddddddddddddddd null_terminated_name relative_position
+proof_trace ::= event*
 
-hook_event := 0xaaaaaaaaaaaaaaaa null_terminated_name hook_arg* 0xbbbbbbbbbbbbbbbb serialized_term
+event       ::= hook
+              | function
+              | rule
+              | config
 
-hook_arg := serialized_term
-          | function_event
-          | hook_event
+argument    ::= hook
+              | function
+              | rule
+              | kore_term
 
-variable := null_terminated_name serialized_term 0xcccccccccccccccc
+name        ::= string
+location    ::= string
+function    ::= WORD(0xDD) name location arg* WORD(0x11)
 
-rule_ordinal := <64-bit unsigned little endian integer>
-rule_arity := <64-bit unsigned little endian integer>
+hook        ::= WORD(0xAA) name arg* WORD(0xBB) kore_term
 
-rewrite_trace := rule_ordinal rule_arity variable* delimited_serial_kore
+ordinal     ::= uint64
+arity       ::= uint64
+variable    ::= name kore_term WORD(0xCC)
+rule        ::= ordinal arity variable*
 
-initial_config := delimited_serial_kore
+config      ::= WORD(0xFF) kore_term WORD(0xCC)
 
-proof_trace := (function_event|hook_event)* initial_config (function_event|hook_event|rewrite_trace)*
+string      ::= <c-style null terminated string>
+uint64      ::= <64-bit unsigned little endian integer>
 ```
 
 ## Notes
 
-- The `rule_arity` should be used to determine how many variable substitutions to read
-- The serialized term for a variable substitution does not begin with the sentinel delimiter.
-  This is because the null terminated variable name can act as the sentinel.
-- The `function_event|hook_event`s at the beginning of the proof_trace are related to configuration initialization.
-- The `relative_position` is a null terminated string of positive integers separated by `:` (ie. `0:1:1`)
+- The `rule_arity` should be used to determine how many variable substitutions
+  to read.
+- Events at the beginning of the trace (i.e. before the first `config` event)
+  are related to configuration initialization.
+- The `relative_position` is a null terminated string of positive integers
+  separated by `:` (ie. `0:1:1`)

Diff for: include/kllvm/codegen/ProofEvent.h

@@ -102,16 +102,23 @@ class ProofEvent {
       llvm::Value *val, KORECompositeSort *sort,
       llvm::BasicBlock *current_block);
 
-  [[nodiscard]] llvm::BasicBlock *rewriteEvent(
-      KOREAxiomDeclaration *axiom, llvm::Value *return_value, uint64_t arity,
+  [[nodiscard]] llvm::BasicBlock *rewriteEvent_pre(
+      KOREAxiomDeclaration *axiom, uint64_t arity,
       std::map<std::string, KOREVariablePattern *> vars,
       llvm::StringMap<llvm::Value *> const &subst,
       llvm::BasicBlock *current_block);
 
-  [[nodiscard]] llvm::BasicBlock *functionEvent(
+  [[nodiscard]] llvm::BasicBlock *rewriteEvent_post(
+      KOREAxiomDeclaration *axiom, llvm::Value *return_value,
+      llvm::BasicBlock *current_block);
+
+  [[nodiscard]] llvm::BasicBlock *functionEvent_pre(
       llvm::BasicBlock *current_block, KORECompositePattern *pattern,
       std::string const &locationStack);
 
+  [[nodiscard]] llvm::BasicBlock *
+  functionEvent_post(llvm::BasicBlock *current_block);
+
 public:
   ProofEvent(KOREDefinition *Definition, llvm::Module *Module)
       : Definition(Definition)

Diff for: lib/codegen/CreateTerm.cpp

@@ -669,6 +669,10 @@ llvm::Value *CreateTerm::createHook(
 llvm::Value *CreateTerm::createFunctionCall(
     std::string name, KORECompositePattern *pattern, bool sret, bool tailcc,
     std::string locationStack) {
+  auto event = ProofEvent(Definition, Module);
+
+  CurrentBlock = event.functionEvent_pre(CurrentBlock, pattern, locationStack);
+
   std::vector<llvm::Value *> args;
   auto returnSort = dynamic_cast<KORECompositeSort *>(
       pattern->getConstructor()->getSort().get());
@@ -697,8 +701,7 @@ llvm::Value *CreateTerm::createFunctionCall(
     }
   }
 
-  auto event = ProofEvent(Definition, Module);
-  CurrentBlock = event.functionEvent(CurrentBlock, pattern, locationStack);
+  CurrentBlock = event.functionEvent_post(CurrentBlock);
 
   return createFunctionCall(name, returnCat, args, sret, tailcc, locationStack);
 }
@@ -1069,10 +1072,8 @@ bool makeFunction(
 
   auto CurrentBlock = creator.getCurrentBlock();
   if (apply && bigStep) {
-    auto event = ProofEvent(definition, Module);
-    CurrentBlock = event.rewriteEvent(
-        axiom, retval, applyRule->arg_end() - applyRule->arg_begin(), vars,
-        subst, CurrentBlock);
+    CurrentBlock = ProofEvent(definition, Module)
+                       .rewriteEvent_post(axiom, retval, CurrentBlock);
   }
 
   if (bigStep) {

Diff for: lib/codegen/Decision.cpp

@@ -2,6 +2,7 @@
 
 #include "kllvm/codegen/CreateTerm.h"
 #include "kllvm/codegen/Debug.h"
+#include "kllvm/codegen/ProofEvent.h"
 #include "kllvm/codegen/Util.h"
 
 #include <llvm/ADT/APInt.h>
@@ -549,6 +550,7 @@ void LeafNode::codegen(Decision *d) {
     setCompleted();
     return;
   }
+
   std::vector<llvm::Value *> args;
   std::vector<llvm::Type *> types;
   for (auto arg : bindings) {
@@ -557,12 +559,36 @@ void LeafNode::codegen(Decision *d) {
     types.push_back(val->getType());
   }
   auto type = getParamType(d->Cat, d->Module);
-  auto Call = llvm::CallInst::Create(
-      getOrInsertFunction(
-          d->Module, name, llvm::FunctionType::get(type, types, false)),
-      args, "", d->CurrentBlock);
+
+  auto applyRule = getOrInsertFunction(
+      d->Module, name, llvm::FunctionType::get(type, types, false));
+
+  // We are generating code for a function with name beginning apply_rule_\d+; to
+  // retrieve the corresponding ordinal we drop the apply_rule_ prefix.
+  auto ordinal = std::stoll(name.substr(11));
+  auto arity = applyRule->arg_end() - applyRule->arg_begin();
+  auto axiom = d->Definition->getAxiomByOrdinal(ordinal);
+
+  auto vars = std::map<std::string, KOREVariablePattern *>{};
+  for (KOREPattern *lhs : axiom->getLeftHandSide()) {
+    lhs->markVariables(vars);
+  }
+  axiom->getRightHandSide()->markVariables(vars);
+
+  auto subst = llvm::StringMap<llvm::Value *>{};
+  auto i = 0;
+  for (auto iter = vars.begin(); iter != vars.end(); ++iter, ++i) {
+    subst[iter->first] = args[i];
+  }
+
+  d->CurrentBlock
+      = ProofEvent(d->Definition, d->Module)
+            .rewriteEvent_pre(axiom, arity, vars, subst, d->CurrentBlock);
+
+  auto Call = llvm::CallInst::Create(applyRule, args, "", d->CurrentBlock);
   setDebugLoc(Call);
   Call->setCallingConv(llvm::CallingConv::Tail);
+
   if (child == nullptr) {
     llvm::ReturnInst::Create(d->Ctx, Call, d->CurrentBlock);
   } else {

Diff for: lib/codegen/ProofEvent.cpp

@@ -211,13 +211,13 @@ llvm::BasicBlock *ProofEvent::hookArg(
  * Rewrite Events
  */
 
-llvm::BasicBlock *ProofEvent::rewriteEvent(
-    KOREAxiomDeclaration *axiom, llvm::Value *return_value, uint64_t arity,
+llvm::BasicBlock *ProofEvent::rewriteEvent_pre(
+    KOREAxiomDeclaration *axiom, uint64_t arity,
     std::map<std::string, KOREVariablePattern *> vars,
     llvm::StringMap<llvm::Value *> const &subst,
     llvm::BasicBlock *current_block) {
   auto [true_block, merge_block, outputFile]
-      = eventPrelude("rewrite", current_block);
+      = eventPrelude("rewrite_pre", current_block);
 
   emitWriteUInt64(outputFile, axiom->getOrdinal(), true_block);
   emitWriteUInt64(outputFile, arity, true_block);
@@ -233,9 +233,22 @@ llvm::BasicBlock *ProofEvent::rewriteEvent(
     emitWriteUInt64(outputFile, word(0xCC), true_block);
   }
 
-  emitWriteUInt64(outputFile, word(0xFF), true_block);
-  emitSerializeConfiguration(outputFile, return_value, true_block);
-  emitWriteUInt64(outputFile, word(0xCC), true_block);
+  llvm::BranchInst::Create(merge_block, true_block);
+  return merge_block;
+}
+
+llvm::BasicBlock *ProofEvent::rewriteEvent_post(
+    KOREAxiomDeclaration *axiom, llvm::Value *return_value,
+    llvm::BasicBlock *current_block) {
+  auto [true_block, merge_block, output_file]
+      = eventPrelude("rewrite_post", current_block);
+
+  auto return_sort = std::dynamic_pointer_cast<KORECompositeSort>(
+      axiom->getRightHandSide()->getSort());
+
+  emitWriteUInt64(output_file, word(0xFF), true_block);
+  emitSerializeTerm(*return_sort, output_file, return_value, true_block);
+  emitWriteUInt64(output_file, word(0xCC), true_block);
 
   llvm::BranchInst::Create(merge_block, true_block);
   return merge_block;
@@ -245,11 +258,11 @@ llvm::BasicBlock *ProofEvent::rewriteEvent(
  * Function Events
  */
 
-llvm::BasicBlock *ProofEvent::functionEvent(
+llvm::BasicBlock *ProofEvent::functionEvent_pre(
     llvm::BasicBlock *current_block, KORECompositePattern *pattern,
     std::string const &locationStack) {
   auto [true_block, merge_block, outputFile]
-      = eventPrelude("function", current_block);
+      = eventPrelude("function_pre", current_block);
 
   std::ostringstream symbolName;
   pattern->getConstructor()->print(symbolName);
@@ -262,4 +275,15 @@ llvm::BasicBlock *ProofEvent::functionEvent(
   return merge_block;
 }
 
+llvm::BasicBlock *
+ProofEvent::functionEvent_post(llvm::BasicBlock *current_block) {
+  auto [true_block, merge_block, outputFile]
+      = eventPrelude("function_post", current_block);
+
+  emitWriteUInt64(outputFile, word(0x11), true_block);
+
+  llvm::BranchInst::Create(merge_block, true_block);
+  return merge_block;
+}
+
 } // namespace kllvm

Diff for: runtime/take_steps.ll

@@ -6,7 +6,7 @@ target triple = "@BACKEND_TARGET_TRIPLE@"
 
 declare tailcc %block* @k_step(%block*)
 declare tailcc %block** @stepAll(%block*, i64*)
-declare void @serializeConfigurationToFile(i8*, %block*)
+declare void @serializeConfigurationToFile(i8*, %block*, i1)
 declare void @writeUInt64ToFile(i8*, i64)
 
 @proof_output = external global i1
@@ -51,7 +51,7 @@ define %block* @take_steps(i64 %depth, %block* %subject) {
 if:
   %output_file = load i8*, i8** @output_file
   call void @writeUInt64ToFile(i8* %output_file, i64 18446744073709551615)
-  call void @serializeConfigurationToFile(i8* %output_file, %block* %subject)
+  call void @serializeConfigurationToFile(i8* %output_file, %block* %subject, i1 1)
   call void @writeUInt64ToFile(i8* %output_file, i64 14757395258967641292)
   br label %merge
 merge:

Diff for: runtime/util/ConfigurationPrinter.cpp

@@ -382,6 +382,7 @@ void printVariableToFile(const char *filename, const char *varname) {
   fprintf(file, "%s", varname);
   char n = 0;
   fwrite(&n, 1, 1, file);
+  fflush(file);
 
   fclose(file);
 }

Diff for: runtime/util/ConfigurationSerializer.cpp

@@ -431,7 +431,7 @@ void serializeTermToFile(
     const char *filename, block *subject, const char *sort) {
   char *data;
   size_t size;
-  serializeConfiguration(subject, sort, &data, &size, false);
+  serializeConfiguration(subject, sort, &data, &size, true);
 
   FILE *file = fopen(filename, "a");
   fwrite(data, 1, size, file);
@@ -444,7 +444,7 @@ void serializeRawTermToFile(
 
   char *data;
   size_t size;
-  serializeConfiguration(term, "SortKItem{}", &data, &size, false);
+  serializeConfiguration(term, "SortKItem{}", &data, &size, true);
 
   FILE *file = fopen(filename, "a");
   fwrite(data, 1, size, file);