Adding support for Machine Integer version of Bytes, List, and MInt functions

config/llvm_header.inc

@@ -245,6 +245,15 @@ define void @take_search_step(ptr %subject) {
   ret void
 }
 
+define i256 @hook_BYTES_length256(ptr %b) {
+entry:
+  %hdr = load i64, ptr %b
+  %len = and i64 %hdr, 1099511627775 ; @LENGTH_MASK@
+  %len_256 = zext i64 %len to i256
+  ret i256 %len_256
+}
+
+
 define ptr @hook_MINT_MInt2Bytes(i256 %mint) {
 entry:
   %alloc = call ptr @kore_alloc(i64 40) ; 8 bytes for header, 32 bytes for MInt

lib/codegen/CreateTerm.cpp

@@ -446,6 +446,38 @@ llvm::Value *create_term::create_hardcoded_hook(
     current_block_ = merge_block;
     return phi;
   }
+  if (name == "BYTES.lengthMInt") {
+    llvm::Value *bytes = alloc_arg(pattern, 0, location_stack);
+    args.push_back(bytes);
+    auto *expected_sort = dynamic_cast<kore_composite_sort *>(
+        pattern->get_constructor()->get_sort().get());
+    unsigned expected_bits = expected_sort->get_category(definition_).bits;
+    llvm::CallInst *result = nullptr;
+    switch (expected_bits) {
+    case 64: {
+      result = llvm::CallInst::Create(
+          get_or_insert_function(
+              module_, "hook_BYTES_length64", llvm::Type::getInt64Ty(ctx_),
+              bytes->getType()),
+          {bytes}, "hook_BYTES_length64", current_block_);
+      break;
+    }
+    case 256: {
+      result = llvm::CallInst::Create(
+          get_or_insert_function(
+              module_, "hook_BYTES_length256",
+              llvm::IntegerType::get(ctx_, 256), bytes->getType()),
+          {bytes}, "hook_BYTES_length256", current_block_);
+      break;
+    }
+    default: {
+      throw std::invalid_argument(
+          fmt::format("BYTES.lengthMInt: unsupported size {}", expected_bits));
+    }
+    }
+    set_debug_loc(result);
+    return result;
+  }
   if (name == "MINT.uvalue") {
     llvm::Value *mint = alloc_arg(pattern, 0, location_stack);
     args.push_back(mint);

runtime/strings/bytes.cpp

@@ -215,6 +215,10 @@ hook_BYTES_memset(SortBytes b, SortInt start, SortInt count, SortInt value) {
   return b;
 }
 
+uint64_t hook_BYTES_length64(SortBytes a) {
+  return len(a);
+}
+
 SortInt hook_BYTES_length(SortBytes a) {
   mpz_t result;
   mpz_init_set_ui(result, len(a));

test/defn/k-files/mints-hook/lengthbytes.k

@@ -0,0 +1,21 @@
+module LENGTHBYTES
+
+imports INT
+imports MINT
+imports BYTES
+imports BOOL
+imports K-EQUAL
+
+    syntax MInt{64}
+    syntax MInt{256} 
+
+    syntax Bytes ::= "bytesString" [macro]
+    rule bytesString =>
+        b"\x1d)0\xdd\xcc#\xeb\x14)Q\x8bAG\xcf\xd46\xa7\xdb\x8f\xc6&\xc1=N\xb6\xa4\x81%\xc2\xd2\xf4o"
+
+    syntax Bool ::= "testLengthBytes" [function]
+    rule testLengthBytes =>
+        lengthBytes(bytesString):Int ==Int MInt2Unsigned(lengthBytes(bytesString):MInt{64}) andBool
+        lengthBytes(bytesString):Int ==Int MInt2Unsigned(lengthBytes(bytesString):MInt{256})
+
+endmodule

test/input/lengthbytes.in

@@ -0,0 +1 @@
+LblinitGeneratedTopCell{}(Lbl'Unds'Map'Unds'{}(Lbl'Stop'Map{}(),Lbl'UndsPipe'-'-GT-Unds'{}(inj{SortKConfigVar{}, SortKItem{}}(\dv{SortKConfigVar{}}("$PGM")),inj{SortBool{}, SortKItem{}}(LbltestLengthBytes'Unds'LENGTHBYTES'Unds'Bool{}()))))

test/output/lengthbytes.out.diff

@@ -0,0 +1 @@
+Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{SortBool{}, SortKItem{}}(\dv{SortBool{}}("true")),dotk{}())),Lbl'-LT-'generatedCounter'-GT-'{}(\dv{SortInt{}}("0")))