btor2tools/
lib.rs

1//! The Btor2Tools package provides a generic parser and tools for the BTOR2 format.
2//!
3//! This crate provides high-level FFI bindings for the [C Btor2Tools package](https://github.com/Boolector/btor2tools).
4//! For a more detailed description of the BTOR2 format, refer to BTOR2, BtorMC and Boolector 3.0. Aina Niemetz, Mathias Preiner, Clifford Wolf, and Armin Biere. CAV 2018.
5//!
6//! # Example
7//!
8//! ```no_run
9//! use std::path::Path;
10//! use btor2tools::Btor2Parser;
11//!
12//! let btor2_file = Path::new("example.btor2");
13//!
14//! Btor2Parser::new()
15//!     .read_lines(&btor2_file)
16//!     .unwrap() // ignore parser error
17//!     .for_each(|line| {
18//!         // print every parsed line
19//!         println!("{:?}", line);
20//!     });
21//! ```
22
23use btor2tools_sys::{
24    btor2parser_delete, btor2parser_error, btor2parser_iter_init, btor2parser_iter_next,
25    btor2parser_new, btor2parser_read_lines, fclose, fopen, Btor2Line as CBtor2Line,
26    Btor2LineIterator as CBtor2LineIterator, Btor2Parser as CBtor2Parser,
27    Btor2SortTag as CBtor2SortTag, Btor2Tag as CBtor2Tag,
28};
29use std::{
30    convert::From,
31    ffi::{CStr, CString},
32    fmt,
33    marker::PhantomData,
34    os::raw::c_char,
35    path::Path,
36    slice,
37};
38use thiserror::Error;
39
40pub struct Btor2Parser {
41    internal: *mut CBtor2Parser,
42}
43
44impl Btor2Parser {
45    pub fn new() -> Self {
46        Self {
47            internal: unsafe { btor2parser_new() },
48        }
49    }
50
51    /// Parses a Btor2 file and returns an iterator to all every formatted line on success.
52    /// On failure, the error includes the line number, where the error occured.
53    pub fn read_lines<P>(&mut self, file: P) -> Result<Btor2LineIterator, Btor2ParserError>
54    where
55        P: AsRef<Path>,
56    {
57        unsafe {
58            let file_path = if let Some(p) = file.as_ref().to_str() {
59                p
60            } else {
61                return Err(Btor2ParserError::InvalidPathEncoding(String::from(
62                    "Path is not UTF-8 encoded",
63                )));
64            };
65
66            let c_file_path = CString::new(file_path).map_err(|_| {
67                Btor2ParserError::InvalidPathEncoding(String::from(
68                    "Path contains a illegal 0 byte",
69                ))
70            })?;
71
72            let c_file_mode = CString::new("r").unwrap();
73
74            let file = fopen(c_file_path.as_ptr(), c_file_mode.as_ptr());
75
76            if file.is_null() {
77                Err(Btor2ParserError::CouldNotOpenFile(file_path.to_owned()))
78            } else {
79                let result = btor2parser_read_lines(self.internal, file);
80
81                fclose(file);
82
83                if result == 0 {
84                    let c_msg = CStr::from_ptr(btor2parser_error(self.internal));
85
86                    Err(Btor2ParserError::SyntaxError(
87                        c_msg
88                            .to_str()
89                            .expect("Btor2tools do not use valid UTF-8 strings")
90                            .to_owned(),
91                    ))
92                } else {
93                    Ok(Btor2LineIterator::new(self))
94                }
95            }
96        }
97    }
98}
99
100impl Drop for Btor2Parser {
101    fn drop(&mut self) {
102        unsafe { btor2parser_delete(self.internal) }
103    }
104}
105
106#[derive(Error, Debug)]
107pub enum Btor2ParserError {
108    #[error("Could not open file: {0}")]
109    CouldNotOpenFile(String),
110
111    #[error("BTOR2 syntax error in {0}")]
112    SyntaxError(String),
113
114    #[error("File path violates encoding rules: {0}")]
115    InvalidPathEncoding(String),
116}
117
118#[derive(Copy, Clone)]
119pub struct Btor2LineIterator<'parser> {
120    parser: PhantomData<&'parser Btor2Parser>,
121    internal: CBtor2LineIterator,
122}
123
124impl<'parser> Btor2LineIterator<'parser> {
125    fn new(parser: &'parser Btor2Parser) -> Self {
126        Self {
127            parser: PhantomData,
128            internal: unsafe { btor2parser_iter_init(parser.internal) },
129        }
130    }
131}
132
133impl<'parser> Iterator for Btor2LineIterator<'parser> {
134    type Item = Btor2Line<'parser>;
135
136    fn next(&mut self) -> Option<Self::Item> {
137        unsafe {
138            let c_line = btor2parser_iter_next(&mut self.internal);
139
140            if c_line.is_null() {
141                None
142            } else {
143                Some(Btor2Line::new(c_line))
144            }
145        }
146    }
147}
148
149#[derive(Clone)]
150pub struct Btor2Line<'parser> {
151    parser: PhantomData<&'parser Btor2Parser>,
152    internal: *const CBtor2Line,
153}
154
155impl<'parser> Btor2Line<'parser> {
156    fn new(internal: *mut CBtor2Line) -> Self {
157        Self {
158            parser: PhantomData,
159            internal,
160        }
161    }
162
163    /// positive id (non zero)
164    pub fn id(&self) -> i64 {
165        unsafe { (*self.internal).id }
166    }
167
168    /// line number in original file
169    pub fn lineno(&self) -> i64 {
170        unsafe { (*self.internal).lineno }
171    }
172
173    /// name in ASCII: "and", "add",...
174    pub fn name(&self) -> &CStr {
175        unsafe { CStr::from_ptr((*self.internal).name) }
176    }
177
178    /// same as name but encoded as enum
179    pub fn tag(&self) -> Btor2Tag {
180        unsafe { Btor2Tag::from((*self.internal).tag) }
181    }
182
183    pub fn sort(&self) -> Btor2Sort {
184        Btor2Sort {
185            line: PhantomData,
186            internal: self.internal,
187        }
188    }
189
190    /// non zero if initialized or has next
191    pub fn init(&self) -> i64 {
192        unsafe { (*self.internal).init }
193    }
194
195    /// non zero if initialized or has next
196    pub fn next(&self) -> i64 {
197        unsafe { (*self.internal).next }
198    }
199
200    /// non zero for const, constd, consth
201    pub fn constant(&self) -> Option<&CStr> {
202        wrap_nullable_c_string(unsafe { (*self.internal).constant })
203    }
204
205    /// optional for: var array state input
206    pub fn symbol(&self) -> Option<&CStr> {
207        wrap_nullable_c_string(unsafe { (*self.internal).symbol })
208    }
209
210    // non zero ids
211    pub fn args(&self) -> &[i64] {
212        unsafe { slice::from_raw_parts((*self.internal).args, (*self.internal).nargs as usize) }
213    }
214}
215
216impl<'parser> fmt::Debug for Btor2Line<'parser> {
217    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
218        f.debug_struct("Btor2Line")
219            .field("id", &self.id())
220            .field("lineno", &self.lineno())
221            .field("name", &self.name())
222            .field("tag", &self.tag())
223            .field("sort", &self.sort())
224            .field("init", &self.init())
225            .field("next", &self.next())
226            .field("constant", &self.constant())
227            .field("symbol", &self.symbol())
228            .field("args", &self.args())
229            .finish()
230    }
231}
232
233#[derive(Copy, Clone)]
234pub struct Btor2Sort<'line, 'parser> {
235    line: PhantomData<&'line Btor2Line<'parser>>,
236    internal: *const CBtor2Line,
237}
238
239impl<'line, 'parser> Btor2Sort<'line, 'parser> {
240    pub fn id(&self) -> i64 {
241        unsafe { (*self.internal).sort.id }
242    }
243
244    pub fn tag(&self) -> Btor2SortTag {
245        unsafe { Btor2SortTag::from((*self.internal).sort.tag) }
246    }
247
248    pub fn name(&self) -> Option<&CStr> {
249        wrap_nullable_c_string(unsafe { (*self.internal).sort.name })
250    }
251
252    pub fn content(&self) -> Btor2SortContent {
253        unsafe {
254            match self.tag() {
255                Btor2SortTag::Array => Btor2SortContent::Array {
256                    index: (*self.internal).sort.__bindgen_anon_1.array.index,
257                    element: (*self.internal).sort.__bindgen_anon_1.array.element,
258                },
259                Btor2SortTag::Bitvec => Btor2SortContent::Bitvec {
260                    width: (*self.internal).sort.__bindgen_anon_1.bitvec.width,
261                },
262            }
263        }
264    }
265}
266
267impl<'line, 'parser> fmt::Debug for Btor2Sort<'line, 'parser> {
268    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
269        f.debug_struct("Btor2Sort")
270            .field("id", &self.id())
271            .field("tag", &self.tag())
272            .field("name", &self.name())
273            .field("content", &self.content())
274            .finish()
275    }
276}
277
278#[derive(Debug, Copy, Clone)]
279pub enum Btor2SortContent {
280    Array { index: i64, element: i64 },
281    Bitvec { width: u32 },
282}
283
284/// BTOR2 tags can be used for fast(er) traversal and operations on BTOR2
285/// format lines, e.g., in a switch statement in client code.
286/// Alternatively, client code can use the name of the BTOR2 tag, which is a C
287/// string (redundantly) contained in the format line. Note that this requires
288/// string comparisons and is therefore slower even if client code uses an
289/// additional hash table.
290#[repr(C)]
291#[derive(Debug, Copy, Clone)]
292pub enum Btor2Tag {
293    Add,
294    And,
295    Bad,
296    Concat,
297    Const,
298    Constraint,
299    Constd,
300    Consth,
301    Dec,
302    Eq,
303    Fair,
304    Iff,
305    Implies,
306    Inc,
307    Init,
308    Input,
309    Ite,
310    Justice,
311    Mul,
312    Nand,
313    Neq,
314    Neg,
315    Next,
316    Nor,
317    Not,
318    One,
319    Ones,
320    Or,
321    Output,
322    Read,
323    Redand,
324    Redor,
325    Redxor,
326    Rol,
327    Ror,
328    Saddo,
329    Sdiv,
330    Sdivo,
331    Sext,
332    Sgt,
333    Sgte,
334    Slice,
335    Sll,
336    Slt,
337    Slte,
338    Sort,
339    Smod,
340    Smulo,
341    Sra,
342    Srem,
343    Srl,
344    Ssubo,
345    State,
346    Sub,
347    Uaddo,
348    Udiv,
349    Uext,
350    Ugt,
351    Ugte,
352    Ult,
353    Ulte,
354    Umulo,
355    Urem,
356    Usubo,
357    Write,
358    Xnor,
359    Xor,
360    Zero,
361}
362
363impl From<CBtor2Tag> for Btor2Tag {
364    fn from(raw: CBtor2Tag) -> Btor2Tag {
365        unsafe { core::mem::transmute(raw) }
366    }
367}
368
369impl Into<CBtor2Tag> for Btor2Tag {
370    fn into(self) -> CBtor2Tag {
371        unsafe { core::mem::transmute(self) }
372    }
373}
374
375#[repr(C)]
376#[derive(Debug, Copy, Clone)]
377pub enum Btor2SortTag {
378    Array,
379    Bitvec,
380}
381
382impl From<CBtor2SortTag> for Btor2SortTag {
383    fn from(raw: CBtor2SortTag) -> Btor2SortTag {
384        unsafe { std::mem::transmute(raw) }
385    }
386}
387
388impl Into<CBtor2SortTag> for Btor2SortTag {
389    fn into(self) -> CBtor2SortTag {
390        unsafe { std::mem::transmute(self) }
391    }
392}
393
394fn wrap_nullable_c_string<'a>(str: *const c_char) -> Option<&'a CStr> {
395    unsafe {
396        if str.is_null() {
397            None
398        } else {
399            Some(CStr::from_ptr(str))
400        }
401    }
402}
btor2tools/lib.rs

btor2tools/
lib.rs
