Merge remote-tracking branch 'origin/develop'

runtimeverification · Aug 22, 2024 · bea1be6 · bea1be6
2 parents 430353d + d194fa1
commit bea1be6
Show file tree

Hide file tree

Showing 2 changed files with 21 additions and 1 deletion.
diff --git a/config/llvm_header.inc b/config/llvm_header.inc
@@ -256,5 +256,25 @@ entry:
   ret i64 %steps
 }
 
+define i1 @hook_MINT_eq_32(i32 %0, i32 %1) {
+  %ret = icmp eq i32 %0, %1
+  ret i1 %ret
+}
+
+define i1 @hook_MINT_eq_64(i64 %0, i64 %1) {
+  %ret = icmp eq i64 %0, %1
+  ret i1 %ret
+}
+
+define i1 @hook_MINT_eq_160(i160 %0, i160 %1) {
+  %ret = icmp eq i160 %0, %1
+  ret i1 %ret
+}
+
+define i1 @hook_MINT_eq_256(i256 %0, i256 %1) {
+  %ret = icmp eq i256 %0, %1
+  ret i1 %ret
+}
+
 attributes #0 = { noreturn }
 )LLVM"
diff --git a/matching/src/main/scala/org/kframework/backend/llvm/matching/pattern/SortCategory.scala b/matching/src/main/scala/org/kframework/backend/llvm/matching/pattern/SortCategory.scala
@@ -663,6 +663,6 @@ case class MIntS(bitwidth: Int) extends SortCategory {
     matrix.compiledCases,
     matrix.compiledDefault
   )
-  def equalityFun: String                  = ???
+  def equalityFun: String                  = "hook_MINT_eq_" + bitwidth
   override def length(rawLength: Int): Int = 1 << bitwidth
 }