Merge remote-tracking branch 'origin/develop'

runtimeverification · Dec 5, 2024 · ea3f2f4 · ea3f2f4
2 parents 19cc319 + dfcadbe
commit ea3f2f4
Show file tree

Hide file tree

Showing 7 changed files with 2,483 additions and 12 deletions.
diff --git a/lib/codegen/CreateStaticTerm.cpp b/lib/codegen/CreateStaticTerm.cpp
@@ -306,10 +306,15 @@ create_static_term::create_token(value_type sort, std::string contents) {
     assert(false && "not implemented yet: tokens");
   case sort_category::MInt: {
     size_t idx = contents.find_first_of("pP");
-    assert(idx != std::string::npos);
-    uint64_t bits = std::stoi(contents.substr(idx + 1));
+    uint64_t bits{};
+    if (idx == std::string::npos) {
+      bits = sort.bits;
+    } else {
+      bits = std::stoi(contents.substr(idx + 1));
+      contents = contents.substr(0, idx);
+    }
     return llvm::ConstantInt::get(
-        llvm::IntegerType::get(ctx_, bits), contents.substr(0, idx), 10);
+        llvm::IntegerType::get(ctx_, bits), contents, 10);
   }
   case sort_category::Bool:
     return llvm::ConstantInt::get(

diff --git a/lib/codegen/EmitConfigParser.cpp b/lib/codegen/EmitConfigParser.cpp
@@ -491,15 +491,18 @@ static void emit_get_token(kore_definition *definition, llvm::Module *module) {
       = llvm::ConstantInt::get(llvm::Type::getInt32Ty(ctx), 0);
   for (auto const &entry : sorts) {
     std::string name = entry.first;
-    if (!entry.second->get_object_sort_variables().empty()) {
-      // TODO: MINT in initial configuration
-      continue;
-    }
     auto sort = kore_composite_sort::create(name);
-    value_type cat = sort->get_category(definition);
-    if (cat.cat == sort_category::Symbol
-        || cat.cat == sort_category::Variable) {
-      continue;
+    value_type cat{};
+    if (entry.second->attributes().contains(attribute_set::key::Hook)
+        && entry.second->attributes().get_string(attribute_set::key::Hook)
+               == "MINT.MInt") {
+      cat.cat = sort_category::MInt;
+    } else {
+      cat = sort->get_category(definition);
+      if (cat.cat == sort_category::Symbol
+          || cat.cat == sort_category::Variable) {
+        continue;
+      }
     }
     current_block->insertInto(func);
     current_block->setName("is_" + name);
@@ -527,10 +530,22 @@ static void emit_get_token(kore_definition *definition, llvm::Module *module) {
     case sort_category::List:
     case sort_category::Set:
     case sort_category::StringBuffer:
-    case sort_category::MInt:
       // TODO: tokens
       add_abort(case_block, module);
       break;
+    case sort_category::MInt: {
+      auto const &len = func->arg_begin() + 1;
+      auto const &contents = func->arg_begin() + 2;
+      auto *get_mint_token = get_or_insert_function(
+          module, "get_mint_token",
+          llvm::FunctionType::get(
+              ptr_ty, {llvm::Type::getInt64Ty(ctx), ptr_ty}, false));
+      auto *mint_token = llvm::CallInst::Create(
+          get_mint_token, {len, contents}, "", case_block);
+      phi->addIncoming(mint_token, case_block);
+      llvm::BranchInst::Create(merge_block, case_block);
+      break;
+    }
     case sort_category::Bool: {
       auto *str = llvm::ConstantDataArray::getString(ctx, "true", false);
       auto *global = module->getOrInsertGlobal("bool_true", str->getType());

diff --git a/matching/src/main/scala/org/kframework/backend/llvm/matching/Generator.scala b/matching/src/main/scala/org/kframework/backend/llvm/matching/Generator.scala
@@ -174,6 +174,8 @@ object Generator {
                 case "false" => "0"
                 case _       => str
               }
+            } else if (hookAtt.contains("MINT.MInt")) {
+              str.substring(0, str.indexOf('p'))
             } else str,
             SortCategory(hookAtt.orElse(Some("STRING.String")), sort, symlib)
           )

diff --git a/runtime/util/ConfigurationParser.cpp b/runtime/util/ConfigurationParser.cpp
@@ -20,6 +20,24 @@ static thread_local Cache cache;
 
 extern "C" {
 
+size_t *hook_MINT_export(mpz_t in, uint64_t bits);
+
+void *get_mint_token(size_t size, char const *c_str) {
+  std::string str = std::string(c_str, size);
+  size_t idx = str.find('p');
+  assert(idx != std::string::npos);
+  std::string precision_str = str.substr(idx + 1);
+  long long precision = std::stoll(precision_str);
+  long long precision_in_bytes = (precision + 7) / 8;
+  char *token = (char *)malloc(precision_in_bytes);
+  std::string val_str = str.substr(0, idx);
+  mpz_t z;
+  mpz_init_set_str(z, val_str.c_str(), 10);
+  size_t *mint = hook_MINT_export(z, precision);
+  memcpy(token, mint, precision_in_bytes);
+  return token;
+}
+
 uint32_t get_tag_for_symbol_name_internal(char const *);
 
 void init_float(floating *result, char const *c_str) {