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

Implementing `hook_LIST_size256` in LLVM IR
Implementing `hook_LIST_size64` in bytes.cpp
Adding `list-size` unit test

Author: Robertorosmaninho

config/llvm_header.inc

@@ -281,6 +281,16 @@ define void @take_search_step(ptr %subject) {
   ret void
 }
 
+; MInt Functions
+
+define i256 @hook_LIST_size256(ptr %l) {
+entry:
+  %len_ptr = getelementptr %list, ptr %l, i64 0, i32 0
+  %len = load i64, ptr %len_ptr
+  %len_256 = zext i64 %len to i256
+  ret i256 %len_256
+}
+
 define i256 @hook_BYTES_get256(ptr %b, i256 %off) {
 entry:
   ; Check for buffer overflow

lib/codegen/CreateTerm.cpp

@@ -446,6 +446,38 @@ llvm::Value *create_term::create_hardcoded_hook(
     current_block_ = merge_block;
     return phi;
   }
+  if (name == "LIST.sizeMInt") {
+    llvm::Value *list = alloc_arg(pattern, 0, location_stack);
+    args.push_back(list);
+    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_LIST_size64", llvm::Type::getInt64Ty(ctx_),
+              list->getType()),
+          {list}, "hook_LIST_size64", current_block_);
+      break;
+    }
+    case 256: {
+      result = llvm::CallInst::Create(
+          get_or_insert_function(
+              module_, "hook_LIST_size256", llvm::IntegerType::get(ctx_, 256),
+              list->getType()),
+          {list}, "hook_LIST_size256", current_block_);
+      break;
+    }
+    default: {
+      throw std::invalid_argument(
+          fmt::format("LIST.sizeMInt: unsupported size {}", expected_bits));
+    }
+    }
+    set_debug_loc(result);
+    return result;
+  }
   if (name == "BYTES.updateMInt") {
     assert(pattern->get_arguments().size() == 3);
     llvm::Value *bytes = alloc_arg(pattern, 0, location_stack);

runtime/collections/lists.cpp

@@ -111,6 +111,10 @@ size_t hook_LIST_size_long(SortList list) {
   return list->size();
 }
 
+uint64_t hook_LIST_size64(SortList list) {
+  return static_cast<uint64_t>(list->size());
+}
+
 SortInt hook_LIST_size(SortList list) {
   mpz_t size;
   mpz_init_set_ui(size, list->size());

test/defn/k-files/mints-hook/list-size.k

@@ -0,0 +1,19 @@
+module LIST-SIZE
+
+imports INT
+imports MINT
+imports BOOL
+imports LIST
+
+    syntax MInt{64}
+    syntax MInt{256} 
+
+    syntax List ::= "listOfMInt" [macro]
+    rule listOfMInt => ListItem(2p64) (ListItem(3p64) (ListItem(4p64) .List))
+
+    syntax Bool ::= "testListSize" [function]
+    rule testListSize =>
+        size(listOfMInt) ==Int MInt2Unsigned(size(listOfMInt)::MInt{64}) andBool
+        size(listOfMInt) ==Int MInt2Unsigned(size(listOfMInt)::MInt{256})
+
+endmodule

test/defn/mints-hook/list-size.kore

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

test/input/list-size.in

@@ -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")))