elina/util.rs
1// Could directly model these types in ast.rs and functions as methods on them,
2// but for the time being this works
3
4use std::ffi::CStr;
5use std::os::raw::c_char;
6use std::ptr::null_mut;
7
8use elina_sys::{elina_lincons0_fprint, elina_lincons0_t, fclose, free, open_memstream};
9
10use crate::ast::{Environment, Manager};
11
12/// This function converts an `elina_lincons0_t` to a `String`.
13///
14/// # Safety
15///
16/// This function necessarily will read from the passed raw pointer, making it unsafe.
17pub unsafe fn lincons0_to_string<M: Manager>(_man: &M, env: &Environment, lincons0: *mut elina_lincons0_t) -> String {
18 let mut buf: *mut c_char = null_mut();
19 let mut len = 0;
20 let fd = open_memstream(&mut buf, &mut len);
21 // to_env_names is okay here, because drop order guarantees it's only dropped after
22 // the function has exited, at which point we don't need to strings anymore
23 let mut env_names = env.to_env_names();
24 elina_lincons0_fprint(fd, lincons0, env_names.as_mut_ptr());
25 fclose(fd);
26 let res = CStr::from_ptr(buf).to_str().unwrap().to_string();
27 free(buf as *mut _);
28 std::mem::drop(env_names);
29 return res;
30 //
31 //
32 // UNFINISHED MANUAL IMPLEMENTATION:
33 //
34 // let linexpr = (*lincons0).linexpr0;
35 // let mut res = linexpr0_to_string(man, env, linexpr);
36 //
37 // match (*lincons0).constyp.into() {
38 // ConsTyp::SUPEQ => res.push_str(" >= 0"),
39 // ConsTyp::SUP => res.push_str(" > 0"),
40 // ConsTyp::EQ => res.push_str(" = 0"),
41 // ConsTyp::DISEQ => res.push_str(" <> 0"),
42 // }
43 //
44 // res
45}
46
47// // https://adventures.michaelfbryan.com/posts/rust-closures-in-ffi/
48// extern "C" fn each_test(i: size_t, dim: elina_dim_t, coeff: *mut elina_coeff_t) {
49// println!("foreach called with: {} {} {:?}", i, dim, coeff);
50//
51// }
52//
53// pub fn linexpr0_to_string<M: Manager>(man: &M, env: &Environment, linexpr0: *mut elina_linexpr0_t) -> String {
54// unsafe {
55// let fd = open_file(CString::new("temp.txt").unwrap().into_raw());
56// let env_names = env.to_env_names();
57// elina_linexpr0_fprint(fd, linexpr0, *env_names);
58// close_file(fd);
59//
60// read_to_string("temp.txt").unwrap()
61// // foreach_linterm_of_linexpr0(linexpr0, Some(each_test))
62// }
63// }
64