From 0a3362fd3e0b65dc795cbc1a85cf46494ae5bb61 Mon Sep 17 00:00:00 2001
From: Guy Repta <50716988+gtrepta@users.noreply.github.com>
Date: Tue, 4 Mar 2025 17:35:44 -0600
Subject: [PATCH 01/11] Initial FFI interface

---
 kframework_ffi/Cargo.lock   |  7 +++++++
 kframework_ffi/Cargo.toml   |  3 +++
 kframework_ffi/src/kllvm.rs | 21 +++++++++++++++++++++
 kframework_ffi/src/lib.rs   |  1 +
 4 files changed, 32 insertions(+)
 create mode 100644 kframework_ffi/Cargo.lock
 create mode 100644 kframework_ffi/Cargo.toml
 create mode 100644 kframework_ffi/src/kllvm.rs
 create mode 100644 kframework_ffi/src/lib.rs

diff --git a/kframework_ffi/Cargo.lock b/kframework_ffi/Cargo.lock
new file mode 100644
index 0000000..1d97779
--- /dev/null
+++ b/kframework_ffi/Cargo.lock
@@ -0,0 +1,7 @@
+# This file is automatically @generated by Cargo.
+# It is not intended for manual editing.
+version = 4
+
+[[package]]
+name = "kframework_ffi"
+version = "0.1.0"
diff --git a/kframework_ffi/Cargo.toml b/kframework_ffi/Cargo.toml
new file mode 100644
index 0000000..5ca9e28
--- /dev/null
+++ b/kframework_ffi/Cargo.toml
@@ -0,0 +1,3 @@
+[package]
+name = "kframework_ffi"
+version = "0.1.0"
diff --git a/kframework_ffi/src/kllvm.rs b/kframework_ffi/src/kllvm.rs
new file mode 100644
index 0000000..4cad081
--- /dev/null
+++ b/kframework_ffi/src/kllvm.rs
@@ -0,0 +1,21 @@
+use std::ffi::{c_char, c_void};
+
+#[repr(C)]
+pub struct block;
+
+#[repr(C)]
+pub struct kore_pattern;
+
+#[allow(dead_code)]
+unsafe extern "C" {
+    pub fn kllvm_init() -> c_void;
+    pub fn kllvm_free_all_memory() -> c_void;
+
+    pub fn take_steps(steps: i64, subject: *const block) -> *const block;
+
+    pub fn kore_pattern_parse(data: *const c_char) -> *const kore_pattern;
+    pub fn kore_pattern_dump(pattern: *const kore_pattern) -> *const c_char;
+
+    pub fn kore_pattern_construct(pattern: *const kore_pattern) -> *const block;
+    pub fn kore_pattern_from_block(subject: *const block) -> *const kore_pattern;
+}
diff --git a/kframework_ffi/src/lib.rs b/kframework_ffi/src/lib.rs
new file mode 100644
index 0000000..4ba78cc
--- /dev/null
+++ b/kframework_ffi/src/lib.rs
@@ -0,0 +1 @@
+pub mod kllvm;

From 7ce006b76e6d6559c456042d2497c559d55ee1fd Mon Sep 17 00:00:00 2001
From: Guy Repta <50716988+gtrepta@users.noreply.github.com>
Date: Sat, 22 Mar 2025 14:30:52 -0500
Subject: [PATCH 02/11] Native wrappers around the FFI

---
 kframework_ffi/src/kllvm.rs |  8 ++++--
 kframework_ffi/src/lib.rs   | 55 ++++++++++++++++++++++++++++++++++++-
 2 files changed, 60 insertions(+), 3 deletions(-)

diff --git a/kframework_ffi/src/kllvm.rs b/kframework_ffi/src/kllvm.rs
index 4cad081..cc43276 100644
--- a/kframework_ffi/src/kllvm.rs
+++ b/kframework_ffi/src/kllvm.rs
@@ -1,10 +1,14 @@
 use std::ffi::{c_char, c_void};
 
 #[repr(C)]
-pub struct block;
+pub struct block {
+    _private: [u8; 0], // Unused field. Makes rust happy about FFI safety.
+}
 
 #[repr(C)]
-pub struct kore_pattern;
+pub struct kore_pattern {
+    _private: [u8; 0], // Unused field. Makes rust happy about FFI safety.
+}
 
 #[allow(dead_code)]
 unsafe extern "C" {
diff --git a/kframework_ffi/src/lib.rs b/kframework_ffi/src/lib.rs
index 4ba78cc..8970d18 100644
--- a/kframework_ffi/src/lib.rs
+++ b/kframework_ffi/src/lib.rs
@@ -1 +1,54 @@
-pub mod kllvm;
+use std::ffi::{CStr, CString};
+mod kllvm;
+
+pub struct KllvmPattern {
+    pattern: *const kllvm::kore_pattern
+}
+
+pub struct KllvmBlock {
+    block: *const kllvm::block
+}
+
+pub fn kllvm_init() { unsafe { kllvm::kllvm_init(); } }
+pub fn kllvm_free_all_memory() { unsafe { kllvm::kllvm_free_all_memory(); } }
+
+pub fn take_steps(steps: i64, subject: KllvmBlock) -> KllvmBlock {
+    let result = unsafe { kllvm::take_steps(steps, subject.block) };
+    KllvmBlock{ block: result }
+}
+
+pub fn kore_pattern_parse(data: &str) -> KllvmPattern {
+    let c_str = CString::new(data).expect("CString::new failed").into_raw();
+    let pattern = unsafe { kllvm::kore_pattern_parse(c_str) };
+    let _ = unsafe { CString::from_raw(c_str) }; // Free the CString memory
+    KllvmPattern { pattern: pattern }
+}
+
+pub fn kore_pattern_dump(pattern: &KllvmPattern) -> String {
+    unsafe {
+        let c_str = kllvm::kore_pattern_dump(pattern.pattern);
+        CStr::from_ptr(c_str).to_str().expect("Failed to convert KllvmPattern to &str").to_string()
+    }
+}
+
+pub fn kore_pattern_construct(pattern: &KllvmPattern) -> KllvmBlock {
+    let block = unsafe { kllvm::kore_pattern_construct(pattern.pattern) };
+    KllvmBlock { block: block }
+}
+
+pub fn kore_pattern_from_block(subject: &KllvmBlock) -> KllvmPattern {
+    let pattern = unsafe { kllvm::kore_pattern_from_block(subject.block) };
+    KllvmPattern { pattern: pattern }
+}
+
+impl From<KllvmPattern> for KllvmBlock {
+    fn from(pattern: KllvmPattern) -> KllvmBlock {
+        kore_pattern_construct(&pattern)
+    }
+}
+
+impl From<KllvmBlock> for KllvmPattern {
+    fn from(block: KllvmBlock) -> KllvmPattern {
+        kore_pattern_from_block(&block)
+    }
+}
\ No newline at end of file

From b8d5256627b2e32e1e4e8400da286a9d70fc21b2 Mon Sep 17 00:00:00 2001
From: Guy Repta <50716988+gtrepta@users.noreply.github.com>
Date: Sat, 22 Mar 2025 21:53:27 -0500
Subject: [PATCH 03/11] Cleanup for when KllvmPattern goes out of scope

---
 kframework_ffi/src/kllvm.rs | 1 +
 kframework_ffi/src/lib.rs   | 6 ++++++
 2 files changed, 7 insertions(+)

diff --git a/kframework_ffi/src/kllvm.rs b/kframework_ffi/src/kllvm.rs
index cc43276..849db41 100644
--- a/kframework_ffi/src/kllvm.rs
+++ b/kframework_ffi/src/kllvm.rs
@@ -19,6 +19,7 @@ unsafe extern "C" {
 
     pub fn kore_pattern_parse(data: *const c_char) -> *const kore_pattern;
     pub fn kore_pattern_dump(pattern: *const kore_pattern) -> *const c_char;
+    pub fn kore_pattern_free(pattern: *const kore_pattern) -> c_void;
 
     pub fn kore_pattern_construct(pattern: *const kore_pattern) -> *const block;
     pub fn kore_pattern_from_block(subject: *const block) -> *const kore_pattern;
diff --git a/kframework_ffi/src/lib.rs b/kframework_ffi/src/lib.rs
index 8970d18..61e25ba 100644
--- a/kframework_ffi/src/lib.rs
+++ b/kframework_ffi/src/lib.rs
@@ -51,4 +51,10 @@ impl From<KllvmBlock> for KllvmPattern {
     fn from(block: KllvmBlock) -> KllvmPattern {
         kore_pattern_from_block(&block)
     }
+}
+
+impl Drop for KllvmPattern {
+    fn drop(&mut self) {
+        unsafe { kllvm::kore_pattern_free(self.pattern) };
+    }
 }
\ No newline at end of file

From df2ac59ce3abbf7995ba0eabb2ec0f2e6de6ce12 Mon Sep 17 00:00:00 2001
From: Guy Repta <50716988+gtrepta@users.noreply.github.com>
Date: Sat, 22 Mar 2025 22:32:39 -0500
Subject: [PATCH 04/11] impl From<KllvmPattern> for String

---
 kframework_ffi/src/lib.rs | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/kframework_ffi/src/lib.rs b/kframework_ffi/src/lib.rs
index 61e25ba..6022f89 100644
--- a/kframework_ffi/src/lib.rs
+++ b/kframework_ffi/src/lib.rs
@@ -41,6 +41,12 @@ pub fn kore_pattern_from_block(subject: &KllvmBlock) -> KllvmPattern {
     KllvmPattern { pattern: pattern }
 }
 
+impl From<KllvmPattern> for String {
+    fn from(pattern: KllvmPattern) -> String {
+        kore_pattern_dump(&pattern)
+    }
+}
+
 impl From<KllvmPattern> for KllvmBlock {
     fn from(pattern: KllvmPattern) -> KllvmBlock {
         kore_pattern_construct(&pattern)

From a27bd46e197670a30ba10a3ce9fb091861e4eb96 Mon Sep 17 00:00:00 2001
From: Guy Repta <50716988+gtrepta@users.noreply.github.com>
Date: Mon, 24 Mar 2025 13:10:44 -0500
Subject: [PATCH 05/11] Free the strings returned by kore_pattern_dump.

These strings are malloc'd, and it's on the caller to free them.
---
 kframework_ffi/src/kllvm.rs | 2 ++
 kframework_ffi/src/lib.rs   | 8 +++++---
 2 files changed, 7 insertions(+), 3 deletions(-)

diff --git a/kframework_ffi/src/kllvm.rs b/kframework_ffi/src/kllvm.rs
index 849db41..6994d3a 100644
--- a/kframework_ffi/src/kllvm.rs
+++ b/kframework_ffi/src/kllvm.rs
@@ -12,6 +12,8 @@ pub struct kore_pattern {
 
 #[allow(dead_code)]
 unsafe extern "C" {
+    pub fn free(ptr: *const c_void) -> c_void;
+
     pub fn kllvm_init() -> c_void;
     pub fn kllvm_free_all_memory() -> c_void;
 
diff --git a/kframework_ffi/src/lib.rs b/kframework_ffi/src/lib.rs
index 6022f89..6bcde4f 100644
--- a/kframework_ffi/src/lib.rs
+++ b/kframework_ffi/src/lib.rs
@@ -1,4 +1,4 @@
-use std::ffi::{CStr, CString};
+use std::ffi::{CStr, CString, c_void};
 mod kllvm;
 
 pub struct KllvmPattern {
@@ -27,7 +27,9 @@ pub fn kore_pattern_parse(data: &str) -> KllvmPattern {
 pub fn kore_pattern_dump(pattern: &KllvmPattern) -> String {
     unsafe {
         let c_str = kllvm::kore_pattern_dump(pattern.pattern);
-        CStr::from_ptr(c_str).to_str().expect("Failed to convert KllvmPattern to &str").to_string()
+        let result = CStr::from_ptr(c_str).to_str().expect("Failed to convert KllvmPattern to &str").to_string();
+        kllvm::free(c_str as *const c_void);
+        result
     }
 }
 
@@ -63,4 +65,4 @@ impl Drop for KllvmPattern {
     fn drop(&mut self) {
         unsafe { kllvm::kore_pattern_free(self.pattern) };
     }
-}
\ No newline at end of file
+}

From 56d54273113114514ffa4bcce81e5d393932ad68 Mon Sep 17 00:00:00 2001
From: Guy Repta <50716988+gtrepta@users.noreply.github.com>
Date: Mon, 24 Mar 2025 13:45:24 -0500
Subject: [PATCH 06/11] Rework kllvm module structure

---
 kframework_ffi/src/kllvm.rs         | 64 +++++++++++++++---------
 kframework_ffi/src/kllvm/block.rs   | 38 ++++++++++++++
 kframework_ffi/src/kllvm/ffi.rs     | 29 +++++++++++
 kframework_ffi/src/kllvm/pattern.rs | 61 +++++++++++++++++++++++
 kframework_ffi/src/lib.rs           | 77 ++++-------------------------
 5 files changed, 177 insertions(+), 92 deletions(-)
 create mode 100644 kframework_ffi/src/kllvm/block.rs
 create mode 100644 kframework_ffi/src/kllvm/ffi.rs
 create mode 100644 kframework_ffi/src/kllvm/pattern.rs

diff --git a/kframework_ffi/src/kllvm.rs b/kframework_ffi/src/kllvm.rs
index 6994d3a..9328678 100644
--- a/kframework_ffi/src/kllvm.rs
+++ b/kframework_ffi/src/kllvm.rs
@@ -1,28 +1,44 @@
-use std::ffi::{c_char, c_void};
+//! # kllvm
+//!
+//! A safe interface for the K framework's llvm backend execution engine.
+//!
+//! This module declares foreign functions which are expected to be linked in
+//! from an external interpreter library built by the kframework.
+//!
+//! ## Example
+//!
+//! ```no_run
+//! use kframework_ffi::kllvm;
+//!
+//! const KORE_STRING: &str = "Lbl'-LT-'generatedTop'-GT-'{}( ...";
+//!
+//! kllvm::init();
+//!
+//! let pattern: kllvm::Pattern = KORE_STRING.parse().expect("Parsing failed!");
+//! let mut block: kllvm::Block = pattern.into();
+//!
+//! block.take_steps(-1);
+//!
+//! let result: kllvm::Pattern = block.into();
+//!
+//! println!("{result}");
+//!
+//! kllvm::free_all_memory();
+//! ```
+mod block;
+mod ffi;
+mod pattern;
 
-#[repr(C)]
-pub struct block {
-    _private: [u8; 0], // Unused field. Makes rust happy about FFI safety.
+pub fn init() {
+    unsafe {
+        ffi::kllvm_init();
+    }
 }
-
-#[repr(C)]
-pub struct kore_pattern {
-    _private: [u8; 0], // Unused field. Makes rust happy about FFI safety.
+pub fn free_all_memory() {
+    unsafe {
+        ffi::kllvm_free_all_memory();
+    }
 }
 
-#[allow(dead_code)]
-unsafe extern "C" {
-    pub fn free(ptr: *const c_void) -> c_void;
-
-    pub fn kllvm_init() -> c_void;
-    pub fn kllvm_free_all_memory() -> c_void;
-
-    pub fn take_steps(steps: i64, subject: *const block) -> *const block;
-
-    pub fn kore_pattern_parse(data: *const c_char) -> *const kore_pattern;
-    pub fn kore_pattern_dump(pattern: *const kore_pattern) -> *const c_char;
-    pub fn kore_pattern_free(pattern: *const kore_pattern) -> c_void;
-
-    pub fn kore_pattern_construct(pattern: *const kore_pattern) -> *const block;
-    pub fn kore_pattern_from_block(subject: *const block) -> *const kore_pattern;
-}
+pub use self::block::Block;
+pub use self::pattern::Pattern;
diff --git a/kframework_ffi/src/kllvm/block.rs b/kframework_ffi/src/kllvm/block.rs
new file mode 100644
index 0000000..e2f2a4b
--- /dev/null
+++ b/kframework_ffi/src/kllvm/block.rs
@@ -0,0 +1,38 @@
+use super::ffi;
+use super::Pattern;
+
+/// A safe wrapper around a foreign pointer to kllvm's interned representation.
+/// kllvm's garbage collector manages the allocation/freeing of this pointer.
+pub struct Block {
+    pub(crate) block: *const ffi::block,
+}
+
+impl Block {
+    pub fn new(pattern: &Pattern) -> Self {
+        let result = unsafe { ffi::kore_pattern_construct(pattern.pattern) };
+        Self { block: result }
+    }
+
+    /// Execute the semantics for a given number of steps over the term.
+    ///
+    /// Pass `-1` to `steps` to execute until no more rules apply.
+    ///
+    /// Note that the current pointer will likely be cleaned up by kllvm's garbage
+    /// collection during execution and will no longer be a valid pointer, so
+    /// the Block will be updated to point at the resulting term.
+    pub fn take_steps(&mut self, steps: i64) {
+        self.block = unsafe { ffi::take_steps(steps, self.block) };
+    }
+}
+
+impl From<Pattern> for Block {
+    fn from(pattern: Pattern) -> Block {
+        Self::new(&pattern)
+    }
+}
+
+impl From<&Pattern> for Block {
+    fn from(pattern: &Pattern) -> Block {
+        Self::new(pattern)
+    }
+}
diff --git a/kframework_ffi/src/kllvm/ffi.rs b/kframework_ffi/src/kllvm/ffi.rs
new file mode 100644
index 0000000..9e997cc
--- /dev/null
+++ b/kframework_ffi/src/kllvm/ffi.rs
@@ -0,0 +1,29 @@
+use std::ffi::{c_char, c_void};
+
+#[repr(C)]
+pub struct block {
+    _private: [u8; 0], // Unused field. Makes rust happy about FFI safety.
+}
+
+#[repr(C)]
+pub struct kore_pattern {
+    _private: [u8; 0], // Unused field. Makes rust happy about FFI safety.
+}
+
+#[allow(dead_code)]
+unsafe extern "C" {
+    /// Some strings from the llvm-backend are malloced, and we need to free them ourselves.
+    pub fn free(ptr: *const c_void) -> c_void;
+
+    pub fn kllvm_init() -> c_void;
+    pub fn kllvm_free_all_memory() -> c_void;
+
+    pub fn take_steps(steps: i64, subject: *const block) -> *const block;
+
+    pub fn kore_pattern_parse(data: *const c_char) -> *const kore_pattern;
+    pub fn kore_pattern_dump(pattern: *const kore_pattern) -> *const c_char;
+    pub fn kore_pattern_free(pattern: *const kore_pattern) -> c_void;
+
+    pub fn kore_pattern_construct(pattern: *const kore_pattern) -> *const block;
+    pub fn kore_pattern_from_block(subject: *const block) -> *const kore_pattern;
+}
diff --git a/kframework_ffi/src/kllvm/pattern.rs b/kframework_ffi/src/kllvm/pattern.rs
new file mode 100644
index 0000000..2638e2b
--- /dev/null
+++ b/kframework_ffi/src/kllvm/pattern.rs
@@ -0,0 +1,61 @@
+use super::ffi;
+use super::Block;
+use std::ffi::{c_void, CStr, CString};
+use std::fmt;
+use std::str::FromStr;
+
+/// A safe wrapper around a pointer to kllvm's kore AST.
+///
+/// kllvm expects the caller to free this object when it's
+/// finished with it. `Drop` is implemented to do this.
+pub struct Pattern {
+    pub(crate) pattern: *const ffi::kore_pattern,
+}
+
+impl Pattern {
+    pub fn new(s: &str) -> Result<Pattern, <Pattern as FromStr>::Err> {
+        Pattern::from_str(s)
+    }
+}
+
+impl FromStr for Pattern {
+    type Err = String;
+
+    fn from_str(s: &str) -> Result<Self, Self::Err> {
+        let c_str = match CString::new(s) {
+            Ok(s) => s.into_raw(),
+            Err(e) => return Err(format!("Error generating CString: {}", e)),
+        };
+        let pattern = unsafe { ffi::kore_pattern_parse(c_str) };
+        let _ = unsafe { CString::from_raw(c_str) }; // Free the CString memory
+        Ok(Self { pattern: pattern })
+    }
+}
+
+impl fmt::Display for Pattern {
+    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
+        let result = unsafe {
+            let c_str = ffi::kore_pattern_dump(self.pattern);
+            let result = CStr::from_ptr(c_str)
+                .to_str()
+                .expect("Failed to convert kllvm::Pattern to &str")
+                .to_string();
+            ffi::free(c_str as *const c_void);
+            result
+        };
+        write!(f, "{}", result)
+    }
+}
+
+impl From<Block> for Pattern {
+    fn from(subject: Block) -> Self {
+        let result = unsafe { ffi::kore_pattern_from_block(subject.block) };
+        Self { pattern: result }
+    }
+}
+
+impl Drop for Pattern {
+    fn drop(&mut self) {
+        unsafe { ffi::kore_pattern_free(self.pattern) };
+    }
+}
diff --git a/kframework_ffi/src/lib.rs b/kframework_ffi/src/lib.rs
index 6bcde4f..8e0784e 100644
--- a/kframework_ffi/src/lib.rs
+++ b/kframework_ffi/src/lib.rs
@@ -1,68 +1,9 @@
-use std::ffi::{CStr, CString, c_void};
-mod kllvm;
-
-pub struct KllvmPattern {
-    pattern: *const kllvm::kore_pattern
-}
-
-pub struct KllvmBlock {
-    block: *const kllvm::block
-}
-
-pub fn kllvm_init() { unsafe { kllvm::kllvm_init(); } }
-pub fn kllvm_free_all_memory() { unsafe { kllvm::kllvm_free_all_memory(); } }
-
-pub fn take_steps(steps: i64, subject: KllvmBlock) -> KllvmBlock {
-    let result = unsafe { kllvm::take_steps(steps, subject.block) };
-    KllvmBlock{ block: result }
-}
-
-pub fn kore_pattern_parse(data: &str) -> KllvmPattern {
-    let c_str = CString::new(data).expect("CString::new failed").into_raw();
-    let pattern = unsafe { kllvm::kore_pattern_parse(c_str) };
-    let _ = unsafe { CString::from_raw(c_str) }; // Free the CString memory
-    KllvmPattern { pattern: pattern }
-}
-
-pub fn kore_pattern_dump(pattern: &KllvmPattern) -> String {
-    unsafe {
-        let c_str = kllvm::kore_pattern_dump(pattern.pattern);
-        let result = CStr::from_ptr(c_str).to_str().expect("Failed to convert KllvmPattern to &str").to_string();
-        kllvm::free(c_str as *const c_void);
-        result
-    }
-}
-
-pub fn kore_pattern_construct(pattern: &KllvmPattern) -> KllvmBlock {
-    let block = unsafe { kllvm::kore_pattern_construct(pattern.pattern) };
-    KllvmBlock { block: block }
-}
-
-pub fn kore_pattern_from_block(subject: &KllvmBlock) -> KllvmPattern {
-    let pattern = unsafe { kllvm::kore_pattern_from_block(subject.block) };
-    KllvmPattern { pattern: pattern }
-}
-
-impl From<KllvmPattern> for String {
-    fn from(pattern: KllvmPattern) -> String {
-        kore_pattern_dump(&pattern)
-    }
-}
-
-impl From<KllvmPattern> for KllvmBlock {
-    fn from(pattern: KllvmPattern) -> KllvmBlock {
-        kore_pattern_construct(&pattern)
-    }
-}
-
-impl From<KllvmBlock> for KllvmPattern {
-    fn from(block: KllvmBlock) -> KllvmPattern {
-        kore_pattern_from_block(&block)
-    }
-}
-
-impl Drop for KllvmPattern {
-    fn drop(&mut self) {
-        unsafe { kllvm::kore_pattern_free(self.pattern) };
-    }
-}
+//! # kframework_ffi
+//!
+//! This crate provides the interface for foreign functions in the K framework.
+//!
+//! ## Notable Interfaces
+//!
+//! - [`kllvm::Pattern`]: kllvm's kore AST.
+//! - [`kllvm::Block`]: kllvm's interned kore representation for execution.
+pub mod kllvm;

From 6562e693a9025b7504d365445c8ac32c23ed2941 Mon Sep 17 00:00:00 2001
From: Guy Repta <50716988+gtrepta@users.noreply.github.com>
Date: Wed, 9 Apr 2025 12:49:09 -0500
Subject: [PATCH 07/11] Example IMP fuzzer using kllvm FFI

---
 examples/fuzzer/Cargo.toml         |  10 +++
 examples/fuzzer/README.md          |  29 ++++++++
 examples/fuzzer/build.rs           |  17 +++++
 examples/fuzzer/k-semantics/fuzz.k |  45 +++++++++++++
 examples/fuzzer/k-semantics/imp.k  |  68 +++++++++++++++++++
 examples/fuzzer/src/main.rs        | 103 +++++++++++++++++++++++++++++
 6 files changed, 272 insertions(+)
 create mode 100644 examples/fuzzer/Cargo.toml
 create mode 100644 examples/fuzzer/README.md
 create mode 100644 examples/fuzzer/build.rs
 create mode 100644 examples/fuzzer/k-semantics/fuzz.k
 create mode 100644 examples/fuzzer/k-semantics/imp.k
 create mode 100644 examples/fuzzer/src/main.rs

diff --git a/examples/fuzzer/Cargo.toml b/examples/fuzzer/Cargo.toml
new file mode 100644
index 0000000..5c47adb
--- /dev/null
+++ b/examples/fuzzer/Cargo.toml
@@ -0,0 +1,10 @@
+[package]
+name = "fuzzer"
+version = "0.1.0"
+edition = "2021"
+
+[dependencies]
+arbitrary = "1.4.1"
+honggfuzz = "0.5.57"
+kframework = { path = "../.." }
+kframework_ffi = { path = "../../kframework_ffi" }
diff --git a/examples/fuzzer/README.md b/examples/fuzzer/README.md
new file mode 100644
index 0000000..2bc9a6a
--- /dev/null
+++ b/examples/fuzzer/README.md
@@ -0,0 +1,29 @@
+# Imp fuzzing with kframework_ffi
+
+This is an example of a fuzzing target for a hashing function that uses the kllvm execution engine for the Imp semantics.
+
+## Requirements
+
+- An installation of the [kframework](https://github.com/runtimeverification/k)
+- An installation of [rustup](https://rustup.rs/)
+- Cargo installed [honggfuzz](https://github.com/rust-fuzz/honggfuzz-rs)
+
+NOTE: If you are using a `kup` installed version of K, then you are very likely to run into linking errors between the nix libraries and your installation of `rustup`. This should be able to get resolved by a proper derivation, but no such thing exists at the time of writing.
+
+## Setup
+
+```
+$ cd k-semantics
+$ kompile --llvm-kompile-type c fuzz.k
+$ export LD_LIBRARY_PATH=$(realpath fuzz-kompiled)
+$ cd ..
+$ cargo hfuzz run fuzzer
+```
+
+## Explanation
+
+The `FUZZ` semantics module extends Imp with an `Assert` statement which rewrites the entire configuration into a failing symbol when it doesn't pass. It also has a success symbol which it will rewrite the configuration to when execution is finished (ie. the <k> cell is empty).
+
+There is an `init_fuzz` utility symbol which takes two integer parameters and then rewrites to an Imp program that performs a hash over those integers. The failure case for this program is arbitrarily if the hash ends up being a very low number.
+
+On the rust side, the fuzzing target uses the random input to construct this `init_fuzz` symbol and the initial configuration in the form of a kore string. Then it uses the foreign functions to build that configuration in kllvm's interned representation, execute it, and retrieve the resulting configuration as another kore string. Then it parses the kore string and checks for the failure or success case.
diff --git a/examples/fuzzer/build.rs b/examples/fuzzer/build.rs
new file mode 100644
index 0000000..9a67992
--- /dev/null
+++ b/examples/fuzzer/build.rs
@@ -0,0 +1,17 @@
+use std::env;
+
+fn main() {
+    // Link interpreter.so
+    println!("cargo:rustc-link-arg=-l:interpreter.so");
+
+    // Add the location of interpreter.so to your LD_LIBRARY_PATH variable
+    // You will also need this variable set when you run the program
+    match env::var_os("LD_LIBRARY_PATH") {
+        Some(paths) => {
+            for lib_path in env::split_paths(&paths) {
+                println!("cargo:rustc-link-search={}", lib_path.display());
+            }
+        }
+        None => (),
+    };
+}
diff --git a/examples/fuzzer/k-semantics/fuzz.k b/examples/fuzzer/k-semantics/fuzz.k
new file mode 100644
index 0000000..7c26c21
--- /dev/null
+++ b/examples/fuzzer/k-semantics/fuzz.k
@@ -0,0 +1,45 @@
+requires "imp.k"
+
+module FUZZ
+  imports IMP
+
+  configuration <T/>
+
+  syntax Stmt ::= "Assert" "(" BExp ")" ";" [strict]
+  rule Assert( true ); => .K
+
+  syntax Pgm   ::= "init_fuzz" "(" Int "," Int ")" [symbol(init_fuzz)]
+  syntax TCell ::= "FUZZ_SUCCESS" [symbol(fuzz_success)]
+                 | "FUZZ_FAILURE" [symbol(fuzz_failure)]
+
+  syntax Id ::= "x" [token]
+              | "y" [token]
+              | "combined" [token]
+              | "salted" [token]
+              | "z" [token]
+              | "hash_val" [token]
+
+  rule <k> init_fuzz(X, Y)
+        => int x, y, combined, salted, z, hash_val;
+
+           x = X;
+           y = Y;
+
+           combined = x * 1000000 + y;
+
+           salted = combined + 1;
+
+           z = salted + 11400714819323198485;
+           z = (z ^ (z >> 30)) * 13787848793156543929;
+           z = (z ^ (z >> 27)) * 10723151780598845931;
+           z = z ^ (z >> 31);
+
+           hash_val = z & 4294967295;
+
+           Assert( !( hash_val <= 15000 ) );
+           ...
+       </k>
+
+  rule <T> <k> .K </k> ... </T> => FUZZ_SUCCESS
+  rule <T> <k> Assert(false); ... </k> ... </T> => FUZZ_FAILURE
+endmodule
diff --git a/examples/fuzzer/k-semantics/imp.k b/examples/fuzzer/k-semantics/imp.k
new file mode 100644
index 0000000..2e545b8
--- /dev/null
+++ b/examples/fuzzer/k-semantics/imp.k
@@ -0,0 +1,68 @@
+// Copyright (c) Runtime Verification, Inc. All Rights Reserved.
+
+module IMP-SYNTAX
+  imports DOMAINS-SYNTAX
+  syntax AExp  ::= Int | Id
+                 | "-" Int
+                 | AExp "*" AExp              [left, strict]
+                 | AExp "^" AExp              [left, strict]
+                 | AExp ">>" AExp             [left, strict]
+                 | AExp "&" AExp             [left, strict]
+                 | "(" AExp ")"               [bracket]
+                 > AExp "+" AExp              [left, strict]
+  syntax BExp  ::= Bool
+                 | AExp "<=" AExp             [seqstrict]
+                 | "!" BExp                   [strict]
+                 | "(" BExp ")"               [bracket]
+                 > BExp "&&" BExp             [left, strict(1)]
+  syntax Block ::= "{" "}"
+                 | "{" Stmt "}"
+  syntax Stmt  ::= Block
+                 | Id "=" AExp ";"            [strict(2)]
+                 | "if" "(" BExp ")"
+                   Block "else" Block         [strict(1)]
+                 | "while" "(" BExp ")" Block
+                 > Stmt Stmt                  [left]
+  syntax Pgm ::= "int" Ids ";" Stmt
+  syntax Ids ::= List{Id,","}
+endmodule
+
+
+module IMP
+  imports IMP-SYNTAX
+  imports DOMAINS
+  syntax KResult ::= Int | Bool
+
+  configuration <T color="yellow">
+                  <k color="green"> $PGM:Pgm </k>
+                  <state color="red"> .Map </state>
+                </T>
+
+// AExp
+  rule <k> X:Id => I ...</k> <state>... X |-> I ...</state>
+  rule I1 * I2 => I1 *Int I2
+  rule I1 ^ I2 => I1 xorInt I2
+  rule I1 >> I2 => I1 >>Int I2
+  rule I1 & I2 => I1 &Int I2
+  rule I1 + I2 => I1 +Int I2
+  rule - I1 => 0 -Int I1
+// BExp
+  rule I1 <= I2 => I1 <=Int I2
+  rule ! T => notBool T
+  rule true && B => B
+  rule false && _ => false
+// Block
+  rule {} => .K
+  rule {S} => S
+// Stmt
+  rule <k> X = I:Int; => .K ...</k> <state>... X |-> (_ => I) ...</state>
+  rule S1:Stmt S2:Stmt => S1 ~> S2
+  rule if (true)  S else _ => S
+  rule if (false) _ else S => S
+  rule while (B) S => if (B) {S while (B) S} else {}
+// Pgm
+  rule <k> int (X,Xs => Xs);_ </k> <state> Rho:Map (.Map => X|->0) </state>
+    requires notBool (X in keys(Rho))
+  rule int .Ids; S => S
+
+endmodule
diff --git a/examples/fuzzer/src/main.rs b/examples/fuzzer/src/main.rs
new file mode 100644
index 0000000..9514343
--- /dev/null
+++ b/examples/fuzzer/src/main.rs
@@ -0,0 +1,103 @@
+use std::panic;
+
+use arbitrary::{Arbitrary, Unstructured};
+use honggfuzz::fuzz;
+use kframework::kore::{App, Parser, Pattern, SymbolId};
+use kframework_ffi::kllvm;
+
+#[derive(Clone, Copy)]
+struct FuzzInput {
+    field1: u32,
+    field2: u32,
+}
+
+impl Arbitrary<'_> for FuzzInput {
+    fn arbitrary(u: &mut Unstructured<'_>) -> arbitrary::Result<Self> {
+        let field1 = u.int_in_range(0..=1000000)?;
+        let field2 = u.int_in_range(0..=1000000)?;
+        Ok(FuzzInput { field1, field2 })
+    }
+}
+
+/// Hardcoded kore strings for assembling the initial configuration
+const PREFIX: &str = r#"
+Lbl'-LT-'generatedTop'-GT-'{}(
+  Lbl'-LT-'T'-GT-'{}(
+    Lbl'-LT-'k'-GT-'{}(
+      kseq{}(inj{SortPgm{}, SortKItem{}}(
+        Lblinit'Unds'fuzz{}(\dv{SortInt{}}(""#;
+const MIDFIX: &str = r#""),\dv{SortInt{}}(""#;
+const POSTFIX: &str = r#""))), dotk{}())), Lbl'-LT-'state'-GT-'{}(Lbl'Stop'Map{}())), Lbl'-LT-'generatedCounter'-GT-'{}(\dv{SortInt{}}("0")))"#;
+
+impl From<FuzzInput> for String {
+    /// Build the kore string to send off to kllvm's parser
+    fn from(input: FuzzInput) -> String {
+        let field1_str = input.field1.to_string();
+        let field2_str = input.field2.to_string();
+
+        format!(
+            "{}{}{}{}{}",
+            PREFIX, field1_str, MIDFIX, field2_str, POSTFIX
+        )
+    }
+}
+
+fn main() {
+    kllvm::init();
+
+    // Free kllvm's memory when panicking.
+    panic::set_hook(Box::new(|_| {
+        kllvm::free_all_memory();
+    }));
+
+    loop {
+        fuzz!(|seed: &[u8]| {
+            let mut u = Unstructured::new(seed);
+            let Ok(input) = FuzzInput::arbitrary(&mut u) else {
+                panic!("Failed to generate input from seed");
+            };
+
+            // Build the initial config, execute it, retrieve the final config kore string
+            let pattern_string: String = input.clone().into();
+            let pattern: kllvm::Pattern =
+                pattern_string.parse().expect("Failed parsing kore string");
+            let mut block: kllvm::Block = pattern.into();
+
+            block.take_steps(-1);
+
+            let result: kllvm::Pattern = block.into();
+
+            // Parse the final kore string as [Pattern] for matching
+            let result_pattern: Pattern = Parser::new(&result.to_string())
+                .unwrap()
+                .pattern()
+                .expect("Failed to parse result pattern");
+
+            match result_pattern {
+                Pattern::App(App { symbol, args, .. }, ..) => {
+                    if symbol == SymbolId::new("Lbl'-LT-'generatedTop'-GT-'".to_string()).unwrap() {
+                        let expected = args
+                            .get(0)
+                            .expect("Expected first argument of generatedTop to be present");
+                        match expected {
+                            Pattern::App(App { symbol, .. }, ..) => {
+                                if *symbol
+                                    == SymbolId::new("Lblfuzz'Unds'failure".to_string()).unwrap()
+                                {
+                                    // <generatedTop> FUZZ_FAILURE </generatedTop>
+                                    panic!("Failure!");
+                                }
+                            }
+                            _ => panic!(
+                                "Expected first argument of generatedTop to be an App pattern"
+                            ),
+                        }
+                    } else {
+                        panic!("Expected symbol for <generatedTop> but found {:?}", symbol);
+                    }
+                }
+                _ => panic!("Expected App pattern but found: {:?}", result_pattern),
+            };
+        });
+    }
+}

From 7aa9622ae7c31f4f37b787ed4d8feec051f0dfcc Mon Sep 17 00:00:00 2001
From: Guy Repta <50716988+gtrepta@users.noreply.github.com>
Date: Mon, 5 May 2025 16:08:55 -0500
Subject: [PATCH 08/11] Dockerfile for fuzzing and CI

---
 .github/actions/with-docker/Dockerfile.fuzz | 26 +++++++++++++++++++++
 .github/actions/with-docker/action.yml      |  6 ++++-
 .github/workflows/test-pr.yml               | 24 +++++++++++++++++++
 3 files changed, 55 insertions(+), 1 deletion(-)
 create mode 100644 .github/actions/with-docker/Dockerfile.fuzz

diff --git a/.github/actions/with-docker/Dockerfile.fuzz b/.github/actions/with-docker/Dockerfile.fuzz
new file mode 100644
index 0000000..8a7bb6a
--- /dev/null
+++ b/.github/actions/with-docker/Dockerfile.fuzz
@@ -0,0 +1,26 @@
+ARG K_VERSION=7.1.241
+ARG RUST_TOOLCHAIN=1.85
+
+# K Image
+FROM runtimeverificationinc/kframework-k:ubuntu-jammy-${K_VERSION} AS semantics
+
+# Build the fuzzing semantics
+WORKDIR /opt/imp-semantics
+COPY examples/fuzzer/k-semantics .
+RUN kompile --llvm-kompile-type c fuzz.k
+
+# Rust Image
+FROM rust:${RUST_TOOLCHAIN}
+
+# Install the kompiled interpreter library
+COPY --from=semantics /opt/imp-semantics/fuzz-kompiled/interpreter.so /usr/lib
+
+# Install honggfuzz
+RUN apt-get update && apt-get install --yes build-essential binutils-dev libunwind-dev libblocksruntime-dev liblzma-dev
+RUN cargo install honggfuzz
+
+# Build the fuzzing target
+WORKDIR /opt/kframework-rs
+COPY . .
+WORKDIR /opt/kframework-rs/examples/fuzzer
+RUN cargo hfuzz build
diff --git a/.github/actions/with-docker/action.yml b/.github/actions/with-docker/action.yml
index 827f6ff..b4389d3 100644
--- a/.github/actions/with-docker/action.yml
+++ b/.github/actions/with-docker/action.yml
@@ -5,6 +5,10 @@ inputs:
     description: 'Docker container name to use'
     required: true
     type: string
+  dockerfile:
+    description: 'Dockerfile to use'
+    required: true
+    type: string
 runs:
   using: 'composite'
   steps:
@@ -15,7 +19,7 @@ runs:
 
       CONTAINER_NAME=${{ inputs.container-name }}
       TAG=runtimeverificationinc/${CONTAINER_NAME}
-      DOCKERFILE=${{ github.action_path }}/Dockerfile
+      DOCKERFILE=${{ github.action_path }}/${{ inputs.dockerfile }}
 
       docker build .         \
         --file ${DOCKERFILE} \
diff --git a/.github/workflows/test-pr.yml b/.github/workflows/test-pr.yml
index f3b39b3..ffb619c 100644
--- a/.github/workflows/test-pr.yml
+++ b/.github/workflows/test-pr.yml
@@ -16,9 +16,33 @@ jobs:
         uses: ./.github/actions/with-docker
         with:
           container-name: kframework-rs-${{ github.sha }}
+          dockerfile: Dockerfile
       - name: 'Build and test'
         run: docker exec -u user kframework-rs-${GITHUB_SHA} make
       - name: 'Tear down Docker'
         if: always()
         run: |
           docker stop --time=0 kframework-rs-${GITHUB_SHA}
+
+  build-ffi-and-fuzz:
+    name: 'Build with the FFI and run the fuzzing example'
+    runs-on: [self-hosted, linux, normal]
+    steps:
+      - name: 'Check out code'
+        uses: actions/checkout@v4
+      - name: 'Set up Docker'
+        uses: ./.github/actions/with-docker
+        with:
+          container-name: kframework-rs-fuzz-${{ github.sha }}
+          dockerfile: Dockerfile.fuzz
+      - name: 'Build and test'
+        run: |
+          export HFUZZ_RUN_ARGS="--verbose --logfile log.txt --run_time 60"
+          docker exec                                \
+            --env HFUZZ_RUN_ARGS="${HFUZZ_RUN_ARGS}" \
+            kframework-rs-fuzz-${GITHUB_SHA}         \
+            cargo hfuzz run fuzzer
+      - name: 'Tear down Docker'
+        if: always()
+        run: |
+          docker stop --time=0 kframework-rs-fuzz-${GITHUB_SHA}

From 77b1c1b3a6a559f798dde979015a785fe5b0dc3b Mon Sep 17 00:00:00 2001
From: Guy Repta <50716988+gtrepta@users.noreply.github.com>
Date: Mon, 5 May 2025 16:42:50 -0500
Subject: [PATCH 09/11] Make Dockerfile.fuzz compatible with user expectations.
 Allow specifying work directory for with-docker

---
 .github/actions/with-docker/Dockerfile.fuzz | 21 +++++++++------------
 .github/actions/with-docker/action.yml      |  6 +++++-
 .github/workflows/test-pr.yml               |  2 ++
 3 files changed, 16 insertions(+), 13 deletions(-)

diff --git a/.github/actions/with-docker/Dockerfile.fuzz b/.github/actions/with-docker/Dockerfile.fuzz
index 8a7bb6a..21d546f 100644
--- a/.github/actions/with-docker/Dockerfile.fuzz
+++ b/.github/actions/with-docker/Dockerfile.fuzz
@@ -1,26 +1,23 @@
 ARG K_VERSION=7.1.241
-ARG RUST_TOOLCHAIN=1.85
+ARG RUST_TOOLCHAIN=1.82.0
 
-# K Image
 FROM runtimeverificationinc/kframework-k:ubuntu-jammy-${K_VERSION} AS semantics
 
-# Build the fuzzing semantics
 WORKDIR /opt/imp-semantics
 COPY examples/fuzzer/k-semantics .
 RUN kompile --llvm-kompile-type c fuzz.k
 
-# Rust Image
 FROM rust:${RUST_TOOLCHAIN}
 
-# Install the kompiled interpreter library
 COPY --from=semantics /opt/imp-semantics/fuzz-kompiled/interpreter.so /usr/lib
-
-# Install honggfuzz
 RUN apt-get update && apt-get install --yes build-essential binutils-dev libunwind-dev libblocksruntime-dev liblzma-dev
 RUN cargo install honggfuzz
 
-# Build the fuzzing target
-WORKDIR /opt/kframework-rs
-COPY . .
-WORKDIR /opt/kframework-rs/examples/fuzzer
-RUN cargo hfuzz build
+ARG USER=user
+ARG GROUP=$USER
+ARG USER_ID=1000
+ARG GROUP_ID=$USER_ID
+
+RUN groupadd -g $GROUP_ID $GROUP && useradd -m -u $USER_ID -s /bin/sh -g $GROUP $USER
+
+USER $USER:$GROUP
diff --git a/.github/actions/with-docker/action.yml b/.github/actions/with-docker/action.yml
index b4389d3..999e7b2 100644
--- a/.github/actions/with-docker/action.yml
+++ b/.github/actions/with-docker/action.yml
@@ -9,6 +9,10 @@ inputs:
     description: 'Dockerfile to use'
     required: true
     type: string
+  workdir:
+    description: 'Work directory for the container'
+    required: true
+    type: string
 runs:
   using: 'composite'
   steps:
@@ -32,7 +36,7 @@ runs:
 
       CONTAINER_NAME=${{ inputs.container-name }}
       TAG=runtimeverificationinc/${CONTAINER_NAME}
-      WORKDIR=/home/user
+      WORKDIR=${{ inputs.workdir }}
 
       docker run                 \
         --name ${CONTAINER_NAME} \
diff --git a/.github/workflows/test-pr.yml b/.github/workflows/test-pr.yml
index ffb619c..32873da 100644
--- a/.github/workflows/test-pr.yml
+++ b/.github/workflows/test-pr.yml
@@ -17,6 +17,7 @@ jobs:
         with:
           container-name: kframework-rs-${{ github.sha }}
           dockerfile: Dockerfile
+          workdir: /home/user
       - name: 'Build and test'
         run: docker exec -u user kframework-rs-${GITHUB_SHA} make
       - name: 'Tear down Docker'
@@ -35,6 +36,7 @@ jobs:
         with:
           container-name: kframework-rs-fuzz-${{ github.sha }}
           dockerfile: Dockerfile.fuzz
+          workdir: /home/user/examples/fuzzer
       - name: 'Build and test'
         run: |
           export HFUZZ_RUN_ARGS="--verbose --logfile log.txt --run_time 60"

From 1f6963404ab6335a273f7f51a8d9b0747d1c86bc Mon Sep 17 00:00:00 2001
From: Guy Repta <50716988+gtrepta@users.noreply.github.com>
Date: Mon, 5 May 2025 16:48:01 -0500
Subject: [PATCH 10/11] Use workdir in docker exec command

---
 .github/actions/with-docker/action.yml | 6 +-----
 .github/workflows/test-pr.yml          | 3 +--
 2 files changed, 2 insertions(+), 7 deletions(-)

diff --git a/.github/actions/with-docker/action.yml b/.github/actions/with-docker/action.yml
index 999e7b2..b4389d3 100644
--- a/.github/actions/with-docker/action.yml
+++ b/.github/actions/with-docker/action.yml
@@ -9,10 +9,6 @@ inputs:
     description: 'Dockerfile to use'
     required: true
     type: string
-  workdir:
-    description: 'Work directory for the container'
-    required: true
-    type: string
 runs:
   using: 'composite'
   steps:
@@ -36,7 +32,7 @@ runs:
 
       CONTAINER_NAME=${{ inputs.container-name }}
       TAG=runtimeverificationinc/${CONTAINER_NAME}
-      WORKDIR=${{ inputs.workdir }}
+      WORKDIR=/home/user
 
       docker run                 \
         --name ${CONTAINER_NAME} \
diff --git a/.github/workflows/test-pr.yml b/.github/workflows/test-pr.yml
index 32873da..fc47f2e 100644
--- a/.github/workflows/test-pr.yml
+++ b/.github/workflows/test-pr.yml
@@ -17,7 +17,6 @@ jobs:
         with:
           container-name: kframework-rs-${{ github.sha }}
           dockerfile: Dockerfile
-          workdir: /home/user
       - name: 'Build and test'
         run: docker exec -u user kframework-rs-${GITHUB_SHA} make
       - name: 'Tear down Docker'
@@ -36,12 +35,12 @@ jobs:
         with:
           container-name: kframework-rs-fuzz-${{ github.sha }}
           dockerfile: Dockerfile.fuzz
-          workdir: /home/user/examples/fuzzer
       - name: 'Build and test'
         run: |
           export HFUZZ_RUN_ARGS="--verbose --logfile log.txt --run_time 60"
           docker exec                                \
             --env HFUZZ_RUN_ARGS="${HFUZZ_RUN_ARGS}" \
+            --workdir /home/user/examples/fuzzer     \
             kframework-rs-fuzz-${GITHUB_SHA}         \
             cargo hfuzz run fuzzer
       - name: 'Tear down Docker'

From 79404496451ae0d1af9963628fcd32c6d3d4a329 Mon Sep 17 00:00:00 2001
From: Guy Repta <50716988+gtrepta@users.noreply.github.com>
Date: Mon, 5 May 2025 16:50:46 -0500
Subject: [PATCH 11/11] Include tail output of hfuzz log

---
 .github/workflows/test-pr.yml | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/.github/workflows/test-pr.yml b/.github/workflows/test-pr.yml
index fc47f2e..041b8e9 100644
--- a/.github/workflows/test-pr.yml
+++ b/.github/workflows/test-pr.yml
@@ -43,6 +43,12 @@ jobs:
             --workdir /home/user/examples/fuzzer     \
             kframework-rs-fuzz-${GITHUB_SHA}         \
             cargo hfuzz run fuzzer
+          echo "Final lines of hfuzz output:"
+          docker exec                                \
+            --env HFUZZ_RUN_ARGS="${HFUZZ_RUN_ARGS}" \
+            --workdir /home/user/examples/fuzzer     \
+            kframework-rs-fuzz-${GITHUB_SHA}         \
+            tail log.txt
       - name: 'Tear down Docker'
         if: always()
         run: |