Improvements to MINT hooks (#1128)

This PR contains a couple different small changes to improve support for MInt in the WASM semantics: * Add implementation of MINT.round, MINT.sext, MINT.umin, MINT.umax, MINT.smin, and MINT.smax. * Add support for equality between machine integers of size 32 and 64 bits. * Add variant of hook_LIST_update which takes an MInt.
runtimeverification · Aug 6, 2024 · 8fe572c · 8fe572c
1 parent 9088cef
commit 8fe572c
Show file tree

Hide file tree

Showing 5 changed files with 83 additions and 6 deletions.
diff --git a/cmake/RuntimeConfig.cmake b/cmake/RuntimeConfig.cmake
@@ -37,6 +37,7 @@ set(VARIABLE_LAYOUT     9)
 set(RANGEMAP_LAYOUT    10)
 set(SETITER_LAYOUT     11)
 set(MAPITER_LAYOUT     12)
+set(MINT_LAYOUT        13)
 
 get_filename_component(INSTALL_DIR_ABS_PATH "${CMAKE_INSTALL_PREFIX}"
                        REALPATH BASE_DIR "${CMAKE_BINARY_DIR}")

diff --git a/config/macros.h b/config/macros.h
@@ -27,6 +27,7 @@
 #define RANGEMAP_LAYOUT @RANGEMAP_LAYOUT@
 #define SETITER_LAYOUT @SETITER_LAYOUT@
 #define MAPITER_LAYOUT @MAPITER_LAYOUT@
+#define MINT_LAYOUT @MINT_LAYOUT@
 
 #define STRINGIFY(x) #x
 #define TOSTRING(X) STRINGIFY(X)

diff --git a/lib/codegen/CreateTerm.cpp b/lib/codegen/CreateTerm.cpp
@@ -565,13 +565,65 @@ llvm::Value *create_term::create_hook(
     }
     return result;
   }
+  if (name == "MINT.round") {
+    llvm::Value *in = alloc_arg(pattern, 0, true, location_stack);
+    auto *type_in = llvm::dyn_cast<llvm::IntegerType>(in->getType());
+    assert(type_in);
+    unsigned bits_in = type_in->getBitWidth();
+    value_type cat_out = dynamic_cast<kore_composite_sort *>(
+                             pattern->get_constructor()->get_sort().get())
+                             ->get_category(definition_);
+    unsigned bits_out = cat_out.bits;
+    auto *type_out = llvm::IntegerType::get(ctx_, bits_out);
+    if (bits_in == bits_out) {
+      // no-op
+      return in;
+    }
+    if (bits_in < bits_out) {
+      return new llvm::ZExtInst(in, type_out, "zext", current_block_);
+    }
+    return new llvm::TruncInst(in, type_out, "trunc", current_block_);
+  }
+  if (name == "MINT.sext") {
+    llvm::Value *in = alloc_arg(pattern, 0, true, location_stack);
+    auto *type_in = llvm::dyn_cast<llvm::IntegerType>(in->getType());
+    assert(type_in);
+    unsigned bits_in = type_in->getBitWidth();
+    value_type cat_out = dynamic_cast<kore_composite_sort *>(
+                             pattern->get_constructor()->get_sort().get())
+                             ->get_category(definition_);
+    unsigned bits_out = cat_out.bits;
+    auto *type_out = llvm::IntegerType::get(ctx_, bits_out);
+    if (bits_in == bits_out) {
+      // no-op
+      return in;
+    }
+    if (bits_in < bits_out) {
+      return new llvm::SExtInst(in, type_out, "sext", current_block_);
+    }
+    return new llvm::TruncInst(in, type_out, "trunc", current_block_);
+  }
   if (name == "MINT.neg") {
     llvm::Value *in = alloc_arg(pattern, 0, true, location_stack);
     return llvm::BinaryOperator::CreateNeg(in, "hook_MINT_neg", current_block_);
   }
   if (name == "MINT.not") {
     llvm::Value *in = alloc_arg(pattern, 0, true, location_stack);
     return llvm::BinaryOperator::CreateNot(in, "hook_MINT_not", current_block_);
+#define MINT_MINMAX(hookname, inst)                                            \
+  }                                                                            \
+  if (name == "MINT." #hookname) {                                             \
+    llvm::Value *first = alloc_arg(pattern, 0, true, location_stack);          \
+    llvm::Value *second = alloc_arg(pattern, 1, true, location_stack);         \
+    auto *cmp = new llvm::ICmpInst(                                            \
+        *current_block_, llvm::CmpInst::inst, first, second,                   \
+        "cmp_" #hookname);                                                     \
+  return llvm::SelectInst::Create(                                             \
+      cmp, first, second, "hook_MINT_" #hookname, current_block_)
+    MINT_MINMAX(umin, ICMP_ULE);
+    MINT_MINMAX(umax, ICMP_UGE);
+    MINT_MINMAX(smin, ICMP_SLE);
+    MINT_MINMAX(smax, ICMP_SGE);
 #define MINT_CMP(hookname, inst)                                               \
   }                                                                            \
   if (name == "MINT." #hookname) {                                             \

diff --git a/runtime/collections/kelemle.cpp b/runtime/collections/kelemle.cpp
@@ -125,6 +125,25 @@ bool hook_KEQUAL_eq(block *arg1, block *arg2) {
           }
           break;
         }
+        case MINT_LAYOUT + 32: {
+          auto *child1ptr = (int32_t *)(child1intptr);
+          auto *child2ptr = (int32_t *)(child2intptr);
+          bool cmp = *child1ptr == *child2ptr;
+          if (!cmp) {
+            return false;
+          }
+          break;
+        }
+        case MINT_LAYOUT + 64: {
+          auto *child1ptr = (int64_t *)(child1intptr);
+          auto *child2ptr = (int64_t *)(child2intptr);
+          bool cmp = *child1ptr == *child2ptr;
+          if (!cmp) {
+            return false;
+          }
+          break;
+        }
+
         default: abort();
         }
       }

diff --git a/runtime/collections/lists.cpp b/runtime/collections/lists.cpp
@@ -113,19 +113,23 @@ list hook_LIST_make(SortInt len, SortKItem value) {
   return {length, value};
 }
 
+list hook_LIST_update_long(SortList list, size_t idx, SortKItem value) {
+  if (idx >= list->size()) {
+    KLLVM_HOOK_INVALID_ARGUMENT(
+        "Index out of range for update: index={}, size={}", idx, list->size());
+  }
+
+  return list->set(idx, value);
+}
+
 list hook_LIST_update(SortList list, SortInt index, SortKItem value) {
   if (!mpz_fits_ulong_p(index)) {
     KLLVM_HOOK_INVALID_ARGUMENT(
         "Length is too large for update: {}", int_to_string(index));
   }
 
   size_t idx = mpz_get_ui(index);
-  if (idx >= list->size()) {
-    KLLVM_HOOK_INVALID_ARGUMENT(
-        "Index out of range for update: index={}, size={}", idx, list->size());
-  }
-
-  return list->set(idx, value);
+  return hook_LIST_update_long(list, idx, value);
 }
 
 list hook_LIST_updateAll(SortList l1, SortInt index, SortList l2) {