Fix type printing in LLVM >= 16 (#861)

This PR fixes
#810, the last
outstanding bit of migration that needed to happen for us to support
LLVM 16+ opaque pointers. The full context for this change is in the
original issue.

To fix the issue, we need to delay the conversion from `ValueType` to
`llvm::Type *` until a deeper point in the call stack when emitting
calls to `addMatchFunction`. The changes here are designed to minimise
the surface area of modified code; we can get away without changing the
`MatchLog` data structure or the `printValueOfType` function by just
converting `ValueType`s to an _imitation_ of the legacy LLVM type
strings. We might want to revisit this architecture in the future, but
for now I'm happy with the design.

The changes made here are tested by the tests for `k-rule-apply`; on
platforms with LLVM 16+ we had marked these tests as expectedly failing,
and we just remove that label here. In the second commit you can see CI
failing because the `XFAIL` is incorrect.

---------

Co-authored-by: rv-jenkins <admin@runtimeverification.com>

include/kllvm/codegen/Decision.h

@@ -2,6 +2,7 @@
 #define DECISION_H
 
 #include "kllvm/ast/AST.h"
+#include "kllvm/codegen/CreateTerm.h"
 #include "kllvm/codegen/DecisionParser.h"
 
 #include <llvm/ADT/APInt.h>
@@ -110,8 +111,8 @@ class DecisionCase {
 
   KORESymbol *getConstructor() const { return constructor; }
   const std::vector<var_type> &getBindings() const { return bindings; }
-  void addBinding(std::string name, llvm::Type *type) {
-    bindings.push_back(std::make_pair(name, type));
+  void addBinding(std::string name, ValueType type, llvm::Module *mod) {
+    bindings.push_back(std::make_pair(name, getParamType(type, mod)));
   }
   llvm::APInt getLiteral() const { return literal; }
   DecisionNode *getChild() const { return child; }
@@ -200,7 +201,7 @@ class MakePatternNode : public DecisionNode {
 class FunctionNode : public DecisionNode {
 private:
   /* the list of arguments to the function. */
-  std::vector<var_type> bindings;
+  std::vector<std::pair<var_type, ValueType>> bindings;
   /* the name of the variable to bind to the result of the function. */
   std::string name;
   /* the name of the function to call */
@@ -226,9 +227,11 @@ class FunctionNode : public DecisionNode {
     return new FunctionNode(name, function, child, cat, type);
   }
 
-  const std::vector<var_type> &getBindings() const { return bindings; }
-  void addBinding(std::string name, llvm::Type *type) {
-    bindings.push_back(std::make_pair(name, type));
+  const std::vector<std::pair<var_type, ValueType>> &getBindings() const {
+    return bindings;
+  }
+  void addBinding(std::string name, ValueType type, llvm::Module *mod) {
+    bindings.push_back({{name, getParamType(type, mod)}, type});
   }
 
   virtual void codegen(Decision *d);
@@ -262,8 +265,8 @@ class LeafNode : public DecisionNode {
   }
 
   const std::vector<var_type> &getBindings() const { return bindings; }
-  void addBinding(std::string name, llvm::Type *type) {
-    bindings.push_back(std::make_pair(name, type));
+  void addBinding(std::string name, ValueType type, llvm::Module *mod) {
+    bindings.push_back(std::make_pair(name, getParamType(type, mod)));
   }
   void setChild(DecisionNode *child) { this->child = child; }
 

include/runtime/header.h

@@ -415,5 +415,6 @@ void init_float2(floating *, std::string);
 std::string intToStringInBase(mpz_t, uint64_t);
 std::string intToString(mpz_t);
 void printValueOfType(
-    std::ostream &os, std::string definitionPath, void *, std::string);
+    std::ostream &os, std::string const &definitionPath, void *value,
+    std::string const &type);
 #endif // RUNTIME_HEADER_H

lib/codegen/Decision.cpp

@@ -373,13 +373,45 @@ void MakePatternNode::codegen(Decision *d) {
   setCompleted();
 }
 
+/*
+ * The code generation step for FunctionNodes emits a call to addMatchFunction
+ * that records why a match failed to apply in the case of side-condition calls
+ * failing. Doing so requires that we store the _type_ of each argument
+ * somewhere, in order that opaque block* values can be safely reinterpreted in
+ * the sort that they originated from (int, bool, symbol, ...). In LLVM versions
+ * < 16, we could encode this information in the LLVM type safely. However,
+ * after the LLVM opaque pointer migration, we can no longer do so (as the
+ * legacy types %mpz* and %block* would both be %ptr, for example). We
+ * therefore define a compatibility translation between sort categories and what
+ * their corresponding LLVM type _would have been_ before opaque pointers.
+ */
+static std::string legacy_value_type_to_string(ValueType sort) {
+  switch (sort.cat) {
+  case SortCategory::Int: return "%mpz*";
+  case SortCategory::Bool: return "i1";
+  case SortCategory::Float: return "%floating*";
+  case SortCategory::Symbol:
+  case SortCategory::Variable: return "%block*";
+
+  // Cases below are deliberately not implemented; the return values are
+  // placeholders to help with debugging only.
+  case SortCategory::Map: return "<map>";
+  case SortCategory::RangeMap: return "<rangemap>";
+  case SortCategory::List: return "<list>";
+  case SortCategory::Set: return "<set>";
+  case SortCategory::StringBuffer: return "<stringbuffer>";
+  case SortCategory::MInt: return "<mint>";
+  case SortCategory::Uncomputed: abort();
+  }
+}
+
 void FunctionNode::codegen(Decision *d) {
   if (beginNode(d, "function" + name)) {
     return;
   }
   std::vector<llvm::Value *> args;
   llvm::StringMap<llvm::Value *> finalSubst;
-  for (auto arg : bindings) {
+  for (auto [arg, cat] : bindings) {
     llvm::Value *val;
     if (arg.first.find_first_not_of("-0123456789") == std::string::npos) {
       val = llvm::ConstantInt::get(
@@ -418,17 +450,18 @@ void FunctionNode::codegen(Decision *d) {
       new llvm::StoreInst(zext, tempAllocCall, d->CurrentBlock);
     }
     functionArgs.push_back(tempAllocCall);
-    for (auto arg : args) {
+    for (auto i = 0u; i < args.size(); ++i) {
+      auto arg = args[i];
+      auto cat = bindings[i].second;
+
       auto tempAllocArg = d->ptrTerm(arg);
       if (arg->getType() == llvm::Type::getInt1Ty(d->Ctx)) {
         llvm::Value *zext = new llvm::ZExtInst(
             Call, llvm::Type::getInt8Ty(d->Ctx), "", d->CurrentBlock);
         new llvm::StoreInst(zext, tempAllocArg, d->CurrentBlock);
       }
       functionArgs.push_back(tempAllocArg);
-      std::string str;
-      llvm::raw_string_ostream output(str);
-      arg->getType()->print(output);
+      auto str = legacy_value_type_to_string(cat);
       functionArgs.push_back(d->stringLiteral(str));
     }
     functionArgs.push_back(

lib/codegen/DecisionParser.cpp

@@ -138,12 +138,10 @@ class DTPreprocessor {
       if (occurrence.size() == 3 && occurrence[0] == "lit"
           && occurrence[2] == "MINT.MInt 64") {
         result->addBinding(
-            occurrence[1],
-            getParamType(KORECompositeSort::getCategory(hook), mod));
+            occurrence[1], KORECompositeSort::getCategory(hook), mod);
       } else {
         result->addBinding(
-            to_string(occurrence),
-            getParamType(KORECompositeSort::getCategory(hook), mod));
+            to_string(occurrence), KORECompositeSort::getCategory(hook), mod);
       }
     }
     return result;
@@ -306,7 +304,7 @@ class DTPreprocessor {
       auto occurrence = vec(get(var, 0));
       auto hook = str(get(var, 1));
       ValueType cat = KORECompositeSort::getCategory(hook);
-      result->addBinding(to_string(occurrence), getParamType(cat, mod));
+      result->addBinding(to_string(occurrence), cat, mod);
     }
     if (auto next = get(node, "next")) {
       auto child = (*this)(next);

runtime/util/ConfigurationPrinter.cpp

@@ -351,8 +351,8 @@ extern "C" void printMatchResult(
 }
 
 void printValueOfType(
-    std::ostream &os, std::string definitionPath, void *value,
-    std::string type) {
+    std::ostream &os, std::string const &definitionPath, void *value,
+    std::string const &type) {
   if (type.compare("%mpz*") == 0) {
     os << reinterpret_cast<mpz_ptr>(value);
   } else if (type.compare("%block*") == 0) {

test/k-rule-apply/definition.kore

@@ -1,4 +1,3 @@
-// XFAIL: opaque-pointers
 // RUN: %kompile %s c
 // RUN: %apply-rule %S TEST.testArray %input-dir/`basename %S`/foo_Array_Success.in %S/definition.o | diff - %output-dir/`basename %S`/foo_Array_Success.out.diff
 // RUN: %apply-rule %S TEST.testArray %input-dir/`basename %S`/foo_Array_Fail.in %S/definition.o | diff - %output-dir/`basename %S`/foo_Array_Fail.out.diff