kframework_ffi: Fixes and Improvements

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<T: Into<String>> From<T> for Str {
@@ -415,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(())
             }
         )*

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<Pattern> for Block {
     fn from(pattern: Pattern) -> Block {
         Self::new(&pattern)

kframework_ffi/src/kllvm/marshal.rs

@@ -126,7 +126,7 @@ impl<H: VarHandler> Marshaller<H> {
     ) -> 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))
     }
 
@@ -136,8 +136,8 @@ impl<H: VarHandler> Marshaller<H> {
         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<H: VarHandler> Marshaller<H> {
         }
     }
 
+    #[allow(unused)]
     fn intern_symbol(
         &mut self,
         id: &kore::SymbolId,
@@ -209,6 +210,15 @@ fn build_sort(s: &kore::Sort) -> Result<Sort, MarshalError> {
     }
 }
 
+fn build_symbol(id: &kore::SymbolId, sorts: &[kore::Sort]) -> Result<Symbol, MarshalError> {
+    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",