From a0319e2e63a436fc0aa64efb0b4dfa673d66a4fc Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Tam=C3=A1s=20T=C3=B3th?=
 <tothtamas28@users.noreply.github.com>
Date: Fri, 8 May 2026 13:27:45 +0000
Subject: [PATCH] Fix `Str` marshalling

---
 kframework_ffi/src/kllvm/marshal.rs |  5 +++--
 kframework_ffi/src/kllvm/pattern.rs | 20 ++++++++++++++++----
 2 files changed, 19 insertions(+), 6 deletions(-)

diff --git a/kframework_ffi/src/kllvm/marshal.rs b/kframework_ffi/src/kllvm/marshal.rs
index 4224311..997095a 100644
--- a/kframework_ffi/src/kllvm/marshal.rs
+++ b/kframework_ffi/src/kllvm/marshal.rs
@@ -8,6 +8,7 @@ pub enum MarshalError {
     Unsupported(&'static str),
     UnknownVar(String),
     Cstring,
+    InvalidString(String, usize),
 }
 
 pub trait VarHandler {
@@ -125,8 +126,8 @@ impl<H: VarHandler> Marshaller<H> {
         value: &kore::Str,
     ) -> Result<(Pattern, bool), MarshalError> {
         let s = build_sort(sort)?;
-        let pattern =
-            Pattern::new_token(value.to_kore().as_str(), &s).map_err(|_| MarshalError::Cstring)?;
+        let pattern = Pattern::new_token(&value.0, &s)
+            .map_err(|i| MarshalError::InvalidString(value.0.clone(), i))?;
         Ok((pattern, true))
     }
 
diff --git a/kframework_ffi/src/kllvm/pattern.rs b/kframework_ffi/src/kllvm/pattern.rs
index 6d1ddad..2fefae2 100644
--- a/kframework_ffi/src/kllvm/pattern.rs
+++ b/kframework_ffi/src/kllvm/pattern.rs
@@ -1,7 +1,7 @@
 use super::ffi;
 use super::{Block, Sort, Symbol};
 use libc;
-use std::ffi::{c_void, CStr, CString, NulError};
+use std::ffi::{c_void, CStr, CString};
 use std::fmt;
 use std::str::FromStr;
 
@@ -30,9 +30,21 @@ impl Pattern {
     }
 
     /// Build a fresh token (Dv) pattern of the given sort.
-    pub fn new_token(value: &str, sort: &Sort) -> Result<Self, NulError> {
-        let c_val = CString::new(value)?;
-        let raw = unsafe { ffi::kore_pattern_new_token(c_val.as_ptr(), sort.sort) };
+    /// Only supports strings that can be Latin-1 encoded.
+    /// On error, returns the index of the first character outside the Latin-1 range.
+    pub fn new_token(value: &str, sort: &Sort) -> Result<Self, usize> {
+        let bytes = value
+            .chars()
+            .enumerate()
+            .map(|(i, c)| u8::try_from(c as u32).map_err(|_| i))
+            .collect::<Result<Vec<_>, _>>()?;
+        let raw = unsafe {
+            ffi::kore_pattern_new_token_with_len(
+                bytes.as_ptr() as *const std::os::raw::c_char,
+                bytes.len(),
+                sort.sort,
+            )
+        };
         Ok(Self { pattern: raw })
     }