complete missing cases

runtimeverification · Aug 19, 2024 · 68f6e5e · 68f6e5e
1 parent bc16f3e
commit 68f6e5e
Show file tree

Hide file tree

Showing 2 changed files with 41 additions and 0 deletions.
diff --git a/runtime/collections/hash.cpp b/runtime/collections/hash.cpp
@@ -19,6 +19,14 @@ __attribute__((always_inline)) void add_hash8(void *h, uint8_t data) {
   hash_length++;
 }
 
+__attribute__((always_inline)) void add_hash32(void *h, uint32_t data) {
+  auto *buf = (uint8_t *)&data;
+  add_hash8(h, buf[0]);
+  add_hash8(h, buf[1]);
+  add_hash8(h, buf[2]);
+  add_hash8(h, buf[3]);
+}
+
 __attribute__((always_inline)) void add_hash64(void *h, uint64_t data) {
   auto *buf = (uint8_t *)&data;
   add_hash8(h, buf[0]);
@@ -116,6 +124,16 @@ void k_hash(block *arg, void *h) {
             k_hash(*childptrptr, h);
             break;
           }
+          case MINT_LAYOUT + 32: {
+            auto *intptr = (uint32_t *)(argintptr + offset);
+            add_hash32(h, *intptr);
+            break;
+          }
+          case MINT_LAYOUT + 64: {
+            auto *intptr = (uint64_t *)(argintptr + offset);
+            add_hash64(h, *intptr);
+            break;
+          }
           case MINT_LAYOUT + 160: {
             auto *intptr = (uint64_t *)(argintptr + offset);
             add_hash64(h, intptr[0]);

diff --git a/runtime/collections/kelemle.cpp b/runtime/collections/kelemle.cpp
@@ -143,6 +143,29 @@ bool hook_KEQUAL_eq(block *arg1, block *arg2) {
           }
           break;
         }
+        case MINT_LAYOUT + 160: {
+          auto *child1ptr = (int64_t *)(child1intptr);
+          auto *child2ptr = (int64_t *)(child2intptr);
+          bool cmp = child1ptr[0] == child2ptr[0]
+                  && child1ptr[1] == child2ptr[1]
+                  && (child1ptr[2] & UINT32_MAX) == (child2ptr[2] & UINT32_MAX);
+          if (!cmp) {
+            return false;
+          }
+          break;
+        }
+        case MINT_LAYOUT + 256: {
+          auto *child1ptr = (int64_t *)(child1intptr);
+          auto *child2ptr = (int64_t *)(child2intptr);
+          bool cmp = child1ptr[0] == child2ptr[0]
+                  && child1ptr[1] == child2ptr[1]
+                  && child1ptr[2] == child2ptr[2]
+                  && child1ptr[3] == child2ptr[3];
+          if (!cmp) {
+            return false;
+          }
+          break;
+        }
 
         default: abort();
         }