Implementing hook_BYTES_updateMInt codegen with support to MInt{256} and MInt{64}

Implementing `hook_BYTES_update256` in LLVM IR
Implementing `hook_BYTES_update64` in bytes.cpp
Adding `bytes-update` unit test

Author: Robertorosmaninho

config/llvm_header.inc

@@ -88,6 +88,8 @@ declare void @error_on_start_substr(i64, i64)
 declare void @error_on_end_substr(ptr, i64)
 declare void @interger_overflow(i64)
 declare void @buffer_overflow_replace_at(i64, i64, i64)
+declare void @buffer_overflow_update(i64, i64)
+declare void @error_on_update(i64)
 declare i1 @hook_BYTES_mutableBytesEnabled()
 
 define ptr @copy_if_needed_in_llvm(ptr %b) {
@@ -522,6 +524,43 @@ entry:
   ret i256 %result
 }
 
+define ptr @hook_BYTES_update256(ptr %b, i256 %index, i256 %value) {
+entry:
+  call ptr @copy_if_needed_in_llvm(ptr %b)
+
+  %hdr = load i64, ptr %b
+  %len = and i64 %hdr, 1099511627775 ; @LENGTH_MASK@
+  %len_256 = zext i64 %len to i256
+
+  %index_uge_len = icmp uge i256 %index, %len_256
+  br i1 %index_uge_len, label %error, label %update_value
+
+error:
+  %index_trunc = trunc i256 %index to i64
+  %len_trunc = trunc i256 %len_256 to i64
+  call void @buffer_overflow_update(i64 %index_trunc, i64 %len_trunc)
+  unreachable
+
+update_value:
+  %value_ge_255 = icmp ugt i256 %value, 255
+  br i1 %value_ge_255, label %error_value, label %set_value
+
+error_value:
+  %value_trunc = trunc i256 %value to i64
+  call void @error_on_update(i64 %value_trunc)
+  unreachable
+
+set_value:
+  %data_ptr = getelementptr i8, ptr %b, i64 8
+  %index_i64 = trunc i256 %index to i64
+  %byte_ptr = getelementptr i8, ptr %data_ptr, i64 %index_i64
+  %value_i8 = trunc i256 %value to i8
+  store i8 %value_i8, ptr %byte_ptr
+
+  ; Return the modified buffer
+  ret ptr %b
+}
+
 
 define i256 @hook_MINT_pow256(i256 %base, i256 %exp) {
 entry:

lib/codegen/CreateTerm.cpp

@@ -446,6 +446,47 @@ llvm::Value *create_term::create_hardcoded_hook(
     current_block_ = merge_block;
     return phi;
   }
+  if (name == "BYTES.updateMInt") {
+    assert(pattern->get_arguments().size() == 3);
+    llvm::Value *bytes = alloc_arg(pattern, 0, location_stack);
+    args.push_back(bytes);
+    llvm::Value *index = alloc_arg(pattern, 1, location_stack);
+    args.push_back(index);
+    llvm::Value *value = alloc_arg(pattern, 2, location_stack);
+    args.push_back(value);
+    auto *index_type = llvm::dyn_cast<llvm::IntegerType>(index->getType());
+    auto *value_type = llvm::dyn_cast<llvm::IntegerType>(value->getType());
+    if (!index_type || !value_type) {
+      throw std::invalid_argument("BYTES.updateMInt: index and/or value "
+                                  "argument is not a machine integer type");
+    }
+    unsigned index_bits = index_type->getBitWidth();
+    llvm::CallInst *result = nullptr;
+    switch (index_bits) {
+    case 64: {
+      result = llvm::CallInst::Create(
+          get_or_insert_function(
+              module_, "hook_BYTES_update64", ptr_ty, bytes->getType(),
+              index_type, value_type),
+          {bytes, index, value}, "hook_BYTES_update64", current_block_);
+      break;
+    }
+    case 256: {
+      result = llvm::CallInst::Create(
+          get_or_insert_function(
+              module_, "hook_BYTES_update256", ptr_ty, bytes->getType(),
+              index_type, value_type),
+          {bytes, index, value}, "hook_BYTES_update256", current_block_);
+      break;
+    }
+    default: {
+      throw std::invalid_argument(
+          fmt::format("BYTES.updateMInt: unsupported size {}", index_bits));
+    }
+    }
+    set_debug_loc(result);
+    return result;
+  }
   if (name == "BYTES.replaceAtMInt") {
     llvm::Value *bytes = alloc_arg(pattern, 0, location_stack);
     args.push_back(bytes);

runtime/strings/bytes.cpp

@@ -74,6 +74,15 @@ void buffer_overflow_replace_at(
       dest_len, src_len);
 }
 
+void buffer_overflow_update(uint64_t len, uint64_t off) {
+  KLLVM_HOOK_INVALID_ARGUMENT(
+      "Buffer overflow on update: off={}, len={}", off, len);
+}
+
+void error_on_update(uint64_t val) {
+  KLLVM_HOOK_INVALID_ARGUMENT(
+      "Not a valid value for a byte in update: {}", val);
+}
 
 // syntax Int ::= Bytes2Int(Bytes, Endianness, Signedness)
 SortInt hook_BYTES_bytes2int(
@@ -205,19 +214,31 @@ uint64_t hook_BYTES_get64(SortBytes b, uint64_t off) {
   return (unsigned char)b->data[off];
 }
 
+SortBytes hook_BYTES_update64(SortBytes b, uint64_t off, uint64_t val) {
+  copy_if_needed(b);
+
+  if (off >= len(b)) {
+    KLLVM_HOOK_INVALID_ARGUMENT(
+        "Buffer overflow on update: off={}, len={}", off, len(b));
+  }
+  if (val >= 256) {
+    KLLVM_HOOK_INVALID_ARGUMENT(
+        "Not a valid value for a byte in update: {}", val);
+  }
+  b->data[off] = (unsigned char)val;
+  return b;
+}
 
 SortBytes hook_BYTES_update(SortBytes b, SortInt off, SortInt val) {
   copy_if_needed(b);
 
   unsigned long off_long = GET_UI(off);
   if (off_long >= len(b)) {
-    KLLVM_HOOK_INVALID_ARGUMENT(
-        "Buffer overflow on update: off={}, len={}", off_long, len(b));
+    buffer_overflow_update(off_long, len(b));
   }
   unsigned long val_long = GET_UI(val);
   if (val_long >= 256) {
-    KLLVM_HOOK_INVALID_ARGUMENT(
-        "Not a valid value for a byte in update: {}", val_long);
+    error_on_update(val_long);
   }
   b->data[off_long] = (unsigned char)val_long;
   return b;

test/defn/k-files/mints-hook/bytes-update.k

@@ -0,0 +1,21 @@
+module BYTES-UPDATE
+
+imports INT
+imports MINT
+imports BYTES
+imports BOOL
+imports K-EQUAL
+
+    syntax MInt{64}
+    syntax MInt{256} 
+
+    syntax Bytes ::= "bytesString" [macro]
+    rule bytesString =>
+        b"a\x00\x1b`\x00\x81`\x0b\x829\xf3`\x01`\x01Us\x8a\n\x19X\x951iBP\xd5p\x04"
+
+    syntax Bool ::= "testBytesUpdate" [function]
+    rule testBytesUpdate =>
+        bytesString[2p64 <- 10p64] ==K bytesString[2 <- 10] andBool
+        bytesString[2p256 <- 10p256] ==K bytesString[2 <- 10]
+    
+endmodule