From 992261907de59826b5dd20599e7792b6d0dd32fa Mon Sep 17 00:00:00 2001 From: Guy Repta <50716988+gtrepta@users.noreply.github.com> Date: Thu, 7 May 2026 19:45:28 -0500 Subject: [PATCH 1/5] fix: Don't try to intern symbols There was a bug here where the 'inj' symbol got interned and was reused for every production with the wrong sorts. The symbol interning is being left unused for now until this is investigated some more. --- kframework_ffi/src/kllvm/marshal.rs | 17 +++++++++++++++-- 1 file changed, 15 insertions(+), 2 deletions(-) diff --git a/kframework_ffi/src/kllvm/marshal.rs b/kframework_ffi/src/kllvm/marshal.rs index 0ada28f..f15b2b7 100644 --- a/kframework_ffi/src/kllvm/marshal.rs +++ b/kframework_ffi/src/kllvm/marshal.rs @@ -136,8 +136,8 @@ impl Marshaller { caching: Caching, ) -> Result<(Pattern, bool), MarshalError> { let mut pattern = { - let sym = self.intern_symbol(&app.symbol, &app.sorts)?; - Pattern::from_symbol(sym) + let sym = build_symbol(&app.symbol, &app.sorts)?; + Pattern::from_symbol(&sym) }; let mut var_free = true; @@ -175,6 +175,7 @@ impl Marshaller { } } + #[allow(unused)] fn intern_symbol( &mut self, id: &kore::SymbolId, @@ -209,6 +210,18 @@ fn build_sort(s: &kore::Sort) -> Result { } } +fn build_symbol( + id: &kore::SymbolId, + sorts: &[kore::Sort], + ) -> Result { + let mut sym = Symbol::new(id.as_str()).map_err(|_| MarshalError::Cstring)?; + for sort in sorts { + let s = build_sort(sort)?; + sym.add_formal_argument(&s); + } + Ok(sym) + } + fn variant_name(p: &kore::Pattern) -> &'static str { match p { kore::Pattern::Var(_) => "Var", From 6b2fd27fa2719b630d814d53191b033403db60fb Mon Sep 17 00:00:00 2001 From: Guy Repta <50716988+gtrepta@users.noreply.github.com> Date: Thu, 7 May 2026 19:49:24 -0500 Subject: [PATCH 2/5] fix: Convert kore::Str back to a kore string for kllvm --- kframework/src/kore/syntax.rs | 26 ++++++++++++++++++++++++++ kframework_ffi/src/kllvm/marshal.rs | 2 +- 2 files changed, 27 insertions(+), 1 deletion(-) diff --git a/kframework/src/kore/syntax.rs b/kframework/src/kore/syntax.rs index 504d573..fb494c2 100644 --- a/kframework/src/kore/syntax.rs +++ b/kframework/src/kore/syntax.rs @@ -228,6 +228,32 @@ impl Str { Ok(Str(chars.into_iter().collect())) } + + pub fn to_kore(&self) -> String { + let mut out = String::new(); + for c in self.0.chars() { + match c { + '"' => out.push_str(r#"\""#), + '\\' => out.push_str(r"\\"), + '\x0c' => out.push_str(r"\f"), + '\n' => out.push_str(r"\n"), + '\r' => out.push_str(r"\r"), + '\t' => out.push_str(r"\t"), + c if (' '..='~').contains(&c) => out.push(c), + c => { + let n = c as u32; + if n <= 0xFF { + out.push_str(&format!(r"\x{:02x}", n)); + } else if n <= 0xFFFF { + out.push_str(&format!(r"\u{:04x}", n)); + } else { + out.push_str(&format!(r"\U{:08x}", n)); + } + } + } + } + out + } } impl> From for Str { diff --git a/kframework_ffi/src/kllvm/marshal.rs b/kframework_ffi/src/kllvm/marshal.rs index f15b2b7..00327f0 100644 --- a/kframework_ffi/src/kllvm/marshal.rs +++ b/kframework_ffi/src/kllvm/marshal.rs @@ -126,7 +126,7 @@ impl Marshaller { ) -> Result<(Pattern, bool), MarshalError> { let s = build_sort(sort)?; let pattern = - Pattern::new_token(value.0.as_str(), &s).map_err(|_| MarshalError::Cstring)?; + Pattern::new_token(value.to_kore().as_str(), &s).map_err(|_| MarshalError::Cstring)?; Ok((pattern, true)) } From 23dcaa97a04466350ae58f7a35554ffd4f72458e Mon Sep 17 00:00:00 2001 From: Guy Repta <50716988+gtrepta@users.noreply.github.com> Date: Thu, 7 May 2026 21:44:17 -0500 Subject: [PATCH 3/5] feat: impl fmt::Display for kllvm::Block --- kframework_ffi/src/kllvm/block.rs | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) diff --git a/kframework_ffi/src/kllvm/block.rs b/kframework_ffi/src/kllvm/block.rs index 1f5ee1b..15a597f 100644 --- a/kframework_ffi/src/kllvm/block.rs +++ b/kframework_ffi/src/kllvm/block.rs @@ -1,5 +1,7 @@ use super::ffi; use super::Pattern; +use std::ffi::{c_void, CStr}; +use std::fmt; /// A safe wrapper around a foreign pointer to kllvm's interned representation. /// kllvm's garbage collector manages the allocation/freeing of this pointer. @@ -25,6 +27,21 @@ impl Block { } } +impl fmt::Display for Block { + fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result { + let result = unsafe { + let c_str = ffi::kore_block_dump(self.block); + let result = CStr::from_ptr(c_str) + .to_str() + .expect("Failed to convert kllvm::Block to &str") + .to_string(); + libc::free(c_str as *mut c_void); + result + }; + write!(f, "{}", result) + } +} + impl From for Block { fn from(pattern: Pattern) -> Block { Self::new(&pattern) From 5683c73c407dd0d2c74cfaa3046c99924e7442c3 Mon Sep 17 00:00:00 2001 From: Guy Repta <50716988+gtrepta@users.noreply.github.com> Date: Thu, 7 May 2026 22:44:21 -0500 Subject: [PATCH 4/5] test: Add test for Str::to_kore --- kframework/src/kore/syntax.rs | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/kframework/src/kore/syntax.rs b/kframework/src/kore/syntax.rs index fb494c2..55def52 100644 --- a/kframework/src/kore/syntax.rs +++ b/kframework/src/kore/syntax.rs @@ -441,10 +441,12 @@ mod tests { let (input, expected) = $value; // When - let actual = Str::from_kore(input)?.0; + let actual = Str::from_kore(input)?; + let roundtrip = actual.to_kore(); // Then - assert_eq!(expected, actual); + assert_eq!(expected, actual.0); + assert_eq!(input.to_lowercase(), roundtrip.to_lowercase()); Ok(()) } )* From 5e3f22485e13ca8ea4a58f254bccf62c63d78c94 Mon Sep 17 00:00:00 2001 From: Guy Repta <50716988+gtrepta@users.noreply.github.com> Date: Thu, 7 May 2026 22:45:06 -0500 Subject: [PATCH 5/5] cleanup: Cargo fmt --- kframework_ffi/src/kllvm/marshal.rs | 17 +++++++---------- 1 file changed, 7 insertions(+), 10 deletions(-) diff --git a/kframework_ffi/src/kllvm/marshal.rs b/kframework_ffi/src/kllvm/marshal.rs index 00327f0..4224311 100644 --- a/kframework_ffi/src/kllvm/marshal.rs +++ b/kframework_ffi/src/kllvm/marshal.rs @@ -210,17 +210,14 @@ fn build_sort(s: &kore::Sort) -> Result { } } -fn build_symbol( - id: &kore::SymbolId, - sorts: &[kore::Sort], - ) -> Result { - let mut sym = Symbol::new(id.as_str()).map_err(|_| MarshalError::Cstring)?; - for sort in sorts { - let s = build_sort(sort)?; - sym.add_formal_argument(&s); - } - Ok(sym) +fn build_symbol(id: &kore::SymbolId, sorts: &[kore::Sort]) -> Result { + let mut sym = Symbol::new(id.as_str()).map_err(|_| MarshalError::Cstring)?; + for sort in sorts { + let s = build_sort(sort)?; + sym.add_formal_argument(&s); } + Ok(sym) +} fn variant_name(p: &kore::Pattern) -> &'static str { match p {