Add raw term symbol to definitions (#907)

This is an alternative formulation to
runtimeverification/k#3829; that PR contains the
original context for why this change is necessary. Rather than adding a
regular symbol to the K standard library source and using a check in the
frontend to ensure that user code doesn't mention it, we directly emit a
symbol into each definition with a name that the frontend cannot
reference.

We also bump the version number for the proof hint format so that this
non-standard symbol must be explicitly accepted by the Python client
code.

Author: Baltoli

include/kllvm/ast/AST.h

@@ -905,6 +905,13 @@ class KOREDefinition {
 
   KORESymbol *injSymbol;
 
+  /*
+   * Insert symbols into this definition that have knowable labels, but cannot
+   * be directly referenced in user code:
+   *   - rawTerm(KItem) for serializing non-symbol backend terms
+   */
+  void insertReservedSymbols();
+
 public:
   static ptr<KOREDefinition> Create() {
     return ptr<KOREDefinition>(new KOREDefinition());

include/kllvm/binary/ProofTraceValidator.h

@@ -152,6 +152,10 @@ class ProofTraceValidator {
       return false;
     }
 
+    if (version != 3) {
+      return false;
+    }
+
     print(fmt::format("version: {}", version));
 
     return true;

include/runtime/header.h

@@ -407,6 +407,7 @@ extern const uint32_t first_inj_tag, last_inj_tag;
 bool is_injection(block *);
 block *strip_injection(block *);
 block *constructKItemInj(void *subject, const char *sort, bool raw_value);
+block *constructRawTerm(void *subject, const char *sort);
 }
 
 std::string floatToString(const floating *);

lib/ast/AST.cpp

@@ -1709,7 +1709,21 @@ void KOREDefinition::addAttribute(sptr<KORECompositePattern> Attribute) {
   attributes.insert({name, std::move(Attribute)});
 }
 
+void KOREDefinition::insertReservedSymbols() {
+  auto mod = KOREModule::Create("K-RAW-TERM");
+  auto decl = KORESymbolDeclaration::Create("rawTerm", true);
+  auto sort = KORECompositeSort::Create("SortKItem");
+
+  decl->getSymbol()->addSort(sort);
+  decl->getSymbol()->addArgument(sort);
+  mod->addDeclaration(std::move(decl));
+
+  addModule(std::move(mod));
+}
+
 void KOREDefinition::preprocess() {
+  insertReservedSymbols();
+
   for (auto iter = axioms.begin(); iter != axioms.end(); ++iter) {
     auto axiom = *iter;
     axiom->pattern = axiom->pattern->expandAliases(this);

runtime/util/ConfigurationSerializer.cpp

@@ -440,7 +440,7 @@ void serializeTermToFile(
 
 void serializeRawTermToFile(
     const char *filename, void *subject, const char *sort) {
-  block *term = constructKItemInj(subject, sort, true);
+  block *term = constructRawTerm(subject, sort);
 
   char *data;
   size_t size;

runtime/util/util.cpp

@@ -29,8 +29,15 @@ block *constructKItemInj(void *subject, const char *sort, bool raw_value) {
   return static_cast<block *>(constructCompositePattern(tag, args));
 }
 
+block *constructRawTerm(void *subject, const char *sort) {
+  auto tag = getTagForSymbolName("rawTerm{}");
+  auto args = std::vector{
+      static_cast<void *>(constructKItemInj(subject, sort, true))};
+  return static_cast<block *>(constructCompositePattern(tag, args));
+}
+
 void printProofHintHeader(char *output_file) {
-  uint32_t version = 2;
+  uint32_t version = 3;
   FILE *file = fopen(output_file, "a");
   fprintf(file, "HINT");
   fwrite(&version, sizeof(version), 1, file);