elina 0.3.1

Safe, high-level Rust wrapper for ELINA
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64

// Could directly model these types in ast.rs and functions as methods on them,
// but for the time being this works

use std::ffi::CStr;
use std::os::raw::c_char;
use std::ptr::null_mut;

use elina_sys::{elina_lincons0_fprint, elina_lincons0_t, fclose, free, open_memstream};

use crate::ast::{Environment, Manager};

/// This function converts an `elina_lincons0_t` to a `String`.
///
/// # Safety
///
/// This function necessarily will read from the passed raw pointer, making it unsafe.
pub unsafe fn lincons0_to_string<M: Manager>(_man: &M, env: &Environment, lincons0: *mut elina_lincons0_t) -> String {
    let mut buf: *mut c_char = null_mut();
    let mut len = 0;
    let fd = open_memstream(&mut buf, &mut len);
    // to_env_names is okay here, because drop order guarantees it's only dropped after
    // the function has exited, at which point we don't need to strings anymore
    let mut env_names = env.to_env_names();
    elina_lincons0_fprint(fd, lincons0, env_names.as_mut_ptr());
    fclose(fd);
    let res = CStr::from_ptr(buf).to_str().unwrap().to_string();
    free(buf as *mut _);
    std::mem::drop(env_names);
    return res;
    //
    //
    // UNFINISHED MANUAL IMPLEMENTATION:
    //
    // let linexpr = (*lincons0).linexpr0;
    // let mut res = linexpr0_to_string(man, env, linexpr);
    //
    // match (*lincons0).constyp.into() {
    //     ConsTyp::SUPEQ => res.push_str(" >= 0"),
    //     ConsTyp::SUP => res.push_str(" > 0"),
    //     ConsTyp::EQ => res.push_str(" = 0"),
    //     ConsTyp::DISEQ => res.push_str(" <> 0"),
    // }
    //
    // res
}

// // https://adventures.michaelfbryan.com/posts/rust-closures-in-ffi/
// extern "C" fn each_test(i: size_t, dim: elina_dim_t, coeff: *mut elina_coeff_t) {
//     println!("foreach called with: {} {} {:?}", i, dim, coeff);
//
// }
//
// pub fn linexpr0_to_string<M: Manager>(man: &M, env: &Environment, linexpr0: *mut elina_linexpr0_t) -> String {
//     unsafe {
//         let fd = open_file(CString::new("temp.txt").unwrap().into_raw());
//         let env_names = env.to_env_names();
//         elina_linexpr0_fprint(fd, linexpr0, *env_names);
//         close_file(fd);
//
//         read_to_string("temp.txt").unwrap()
//         // foreach_linterm_of_linexpr0(linexpr0, Some(each_test))
//     }
// }