flussab_btor2/
parser.rs

1use std::{
2    borrow::Borrow,
3    io::{BufReader, Read},
4};
5
6use bstr::BString;
7use flussab::{text::LineReader, DeferredReader, Parsed};
8
9use crate::{
10    btor2::{
11        Array, Assignment, BinaryConst, Const, DecimalConst, HexConst, Line, Node, NodeId,
12        NodeVariant, Op, Output, SingleValueOutput, Sort, UnaryOp, Value, ValueVariant,
13    },
14    error::ParseError,
15    token::{self, NodeToken, NodeValueToken},
16};
17
18/// Configuration options for BTOR2 parsing.
19#[derive(Default)]
20#[non_exhaustive]
21pub struct Config {}
22
23/// A BTOR2 parser.
24pub struct Parser<'a> {
25    reader: LineReader<'a>,
26    node_buf: Vec<NodeId>,
27    const_buf: String,
28    symbol_buf: BString,
29}
30
31impl<'a> Parser<'a> {
32    /// Creates a parser reading from a [`LineReader`].
33    pub fn new(reader: LineReader<'a>, config: Config) -> Result<Self, ParseError> {
34        let Config {} = config;
35        Ok(Self {
36            reader,
37            node_buf: Default::default(),
38            const_buf: Default::default(),
39            symbol_buf: Default::default(),
40        })
41    }
42
43    /// Creates a parser reading from a [`BufReader`].
44    pub fn from_buf_reader(
45        buf_reader: BufReader<impl Read + 'a>,
46        config: Config,
47    ) -> Result<Self, ParseError> {
48        Self::new(
49            LineReader::new(DeferredReader::from_buf_reader(buf_reader)),
50            config,
51        )
52    }
53
54    /// Creates a parser reading from a [`Read`] instance.
55    ///
56    /// If the [`Read`] instance is a [`BufReader`], it is better to use
57    /// [`from_buf_reader`][Self::from_buf_reader] to avoid unnecessary double buffering of the
58    /// data.
59    pub fn from_read(read: impl Read + 'a, config: Config) -> Result<Self, ParseError> {
60        Self::new(LineReader::new(DeferredReader::from_read(read)), config)
61    }
62
63    /// Creates a parser reading from a boxed [`Read`] instance.
64    ///
65    /// If the [`Read`] instance is a [`BufReader`], it is better to use
66    /// [`from_buf_reader`][Self::from_buf_reader] to avoid unnecessary double buffering of the
67    /// data.
68    #[inline(never)]
69    pub fn from_boxed_dyn_read(
70        read: Box<dyn Read + 'a>,
71        config: Config,
72    ) -> Result<Self, ParseError> {
73        Self::new(
74            LineReader::new(DeferredReader::from_boxed_dyn_read(read)),
75            config,
76        )
77    }
78    fn try_node(&mut self) -> Parsed<Node<'static>, ParseError> {
79        token::node_id(&mut self.reader).and_then(|node_id| {
80            token::required_space(&mut self.reader)?;
81            let node_token = token::node_token(&mut self.reader)
82                .or_give_up(|| token::unexpected(&mut self.reader, "node keyword"))?;
83            let variant = match node_token {
84                NodeToken::Sort => NodeVariant::Sort({
85                    token::required_space(&mut self.reader)?;
86                    match token::sort_token(&mut self.reader)
87                        .or_give_up(|| token::unexpected(&mut self.reader, "sort keyword"))?
88                    {
89                        token::SortToken::Bitvec => {
90                            token::required_space(&mut self.reader)?;
91                            let width =
92                                token::required_positive_int(&mut self.reader, "bit width")?;
93                            Sort::BitVec(width)
94                        }
95                        token::SortToken::Array => {
96                            token::required_space(&mut self.reader)?;
97                            let domain = token::required_sort_id(&mut self.reader)?;
98                            token::required_space(&mut self.reader)?;
99                            let codomain = token::required_sort_id(&mut self.reader)?;
100
101                            Sort::Array(Array(domain, codomain))
102                        }
103                    }
104                }),
105                NodeToken::Assignment(kind) => {
106                    token::required_space(&mut self.reader)?;
107                    let sort = token::required_sort_id(&mut self.reader)?;
108                    token::required_space(&mut self.reader)?;
109                    let state = token::required_node_id(&mut self.reader)?;
110                    token::required_space(&mut self.reader)?;
111                    let value = token::required_node_id(&mut self.reader)?;
112
113                    NodeVariant::Assignment(Assignment {
114                        state,
115                        sort,
116                        kind,
117                        value,
118                    })
119                }
120                NodeToken::Output(kind) => {
121                    token::required_space(&mut self.reader)?;
122                    let value = token::required_node_id(&mut self.reader)?;
123                    NodeVariant::Output(Output::SingleValue(SingleValueOutput { kind, value }))
124                }
125                NodeToken::Justice => {
126                    token::required_space(&mut self.reader)?;
127                    let count =
128                        token::required_positive_int(&mut self.reader, "condition count")?.get();
129                    self.node_buf.clear();
130                    for _ in 0..count {
131                        token::required_space(&mut self.reader)?;
132                        let condition = token::required_node_id(&mut self.reader)?;
133                        self.node_buf.push(condition);
134                    }
135                    NodeVariant::Output(Output::Justice(&[]))
136                }
137                NodeToken::Value(value_token) => NodeVariant::Value({
138                    token::required_space(&mut self.reader)?;
139                    let sort = token::required_sort_id(&mut self.reader)?;
140
141                    let variant = match value_token {
142                        NodeValueToken::Const => {
143                            token::required_space(&mut self.reader)?;
144                            self.const_buf.clear();
145                            self.const_buf
146                                .push_str(token::required_binary_constant(&mut self.reader)?);
147
148                            ValueVariant::Const(Const::Binary(BinaryConst("")))
149                        }
150                        NodeValueToken::Constd => {
151                            token::required_space(&mut self.reader)?;
152                            self.const_buf.clear();
153                            self.const_buf
154                                .push_str(token::required_decimal_constant(&mut self.reader)?);
155
156                            ValueVariant::Const(Const::Decimal(DecimalConst("")))
157                        }
158                        NodeValueToken::Consth => {
159                            token::required_space(&mut self.reader)?;
160                            self.const_buf.clear();
161                            self.const_buf
162                                .push_str(token::required_hex_constant(&mut self.reader)?);
163
164                            ValueVariant::Const(Const::Hex(HexConst("")))
165                        }
166                        NodeValueToken::Ones => ValueVariant::Const(Const::Ones),
167                        NodeValueToken::One => ValueVariant::Const(Const::One),
168                        NodeValueToken::Zero => ValueVariant::Const(Const::Zero),
169
170                        NodeValueToken::Input => ValueVariant::Input,
171                        NodeValueToken::State => ValueVariant::State,
172                        NodeValueToken::ExtOp(ext_op_token) => {
173                            token::required_space(&mut self.reader)?;
174                            let a0 = token::required_node_id(&mut self.reader)?;
175                            token::required_space(&mut self.reader)?;
176                            let pad =
177                                token::required_nonnegative_int(&mut self.reader, "pad width")?;
178
179                            ValueVariant::Op(Op::Unary(ext_op_token.unary_op(pad), a0))
180                        }
181                        NodeValueToken::Slice => {
182                            token::required_space(&mut self.reader)?;
183                            let a0 = token::required_node_id(&mut self.reader)?;
184                            token::required_space(&mut self.reader)?;
185                            let u = token::required_nonnegative_int(&mut self.reader, "bit index")?;
186                            token::required_space(&mut self.reader)?;
187                            let l = token::required_nonnegative_int(&mut self.reader, "bit index")?;
188
189                            ValueVariant::Op(Op::Unary(UnaryOp::Slice(u, l), a0))
190                        }
191
192                        NodeValueToken::UnaryOp(unary_op_token) => {
193                            token::required_space(&mut self.reader)?;
194                            let a0 = token::required_node_id(&mut self.reader)?;
195
196                            ValueVariant::Op(Op::Unary(unary_op_token.unary_op(), a0))
197                        }
198
199                        NodeValueToken::BinaryOp(binary_op) => {
200                            token::required_space(&mut self.reader)?;
201                            let a0 = token::required_node_id(&mut self.reader)?;
202                            token::required_space(&mut self.reader)?;
203                            let a1 = token::required_node_id(&mut self.reader)?;
204                            ValueVariant::Op(Op::Binary(binary_op, [a0, a1]))
205                        }
206
207                        NodeValueToken::TernaryOp(ternary_op) => {
208                            token::required_space(&mut self.reader)?;
209                            let a0 = token::required_node_id(&mut self.reader)?;
210                            token::required_space(&mut self.reader)?;
211                            let a1 = token::required_node_id(&mut self.reader)?;
212                            token::required_space(&mut self.reader)?;
213                            let a2 = token::required_node_id(&mut self.reader)?;
214                            ValueVariant::Op(Op::Ternary(ternary_op, [a0, a1, a2]))
215                        }
216                    };
217
218                    Value { sort, variant }
219                }),
220            };
221
222            let (symbol, comment) = token::space(&mut self.reader)
223                .and_then(|_| {
224                    token::comment_start(&mut self.reader)
225                        .map(|_| (None, Some("".into())))
226                        .or_parse(|| {
227                            token::symbol_name(&mut self.reader)
228                                .map(|symbol| {
229                                    self.symbol_buf.clear();
230                                    self.symbol_buf.extend_from_slice(symbol);
231                                    Some("".into())
232                                })
233                                .and_then(|symbol| {
234                                    token::space(&mut self.reader)
235                                        .and_then(|_| {
236                                            token::comment_start(&mut self.reader)
237                                                .map(|_| (symbol, Some("".into())))
238                                                .or_give_up(|| {
239                                                    token::unexpected(&mut self.reader, "comment")
240                                                })
241                                        })
242                                        .or_parse(|| {
243                                            token::newline(&mut self.reader)
244                                                .and_then(|_| Ok((symbol, None)))
245                                        })
246                                        .or_give_up(|| {
247                                            token::unexpected(
248                                                &mut self.reader,
249                                                concat!(
250                                                    "end of line or ",
251                                                    "a space character followed by a comment"
252                                                ),
253                                            )
254                                        })
255                                })
256                        })
257                        .or_give_up(|| {
258                            token::unexpected(&mut self.reader, "symbol name or comment")
259                        })
260                })
261                .or_parse(|| token::newline(&mut self.reader).and_then(|_| Ok((None, None))))
262                .or_give_up(|| {
263                    token::unexpected(
264                        &mut self.reader,
265                        "end of line, a space character followed by a symbol name or comment",
266                    )
267                })?;
268
269            Ok(Node {
270                id: node_id,
271                variant,
272                symbol,
273                comment,
274            })
275        })
276    }
277
278    fn try_comment(&mut self) -> Parsed<(), ParseError> {
279        token::comment_start(&mut self.reader)
280    }
281
282    /// Parses the next line of the BTOR2 file.
283    ///
284    /// Returns `Ok(None)` when reaching the end of the file.
285    pub fn next_line(&mut self) -> Result<Option<Line>, ParseError> {
286        token::skip_whitespace(&mut self.reader);
287
288        let Some(mut node) = self
289            .try_node()
290            .map(Line::Node)
291            .or_parse(|| self.try_comment().map(|()| Line::Comment("".into())))
292            .map(Some)
293            .or_parse(|| token::eof(&mut self.reader).map(|_| None))
294            .or_give_up(|| token::unexpected(&mut self.reader, "btor2 line"))?
295        else {
296            self.reader.reader.check_io_error()?;
297            return Ok(None);
298        };
299
300        if node.has_comment() {
301            node.update_comment(token::comment_body(&mut self.reader));
302        }
303
304        node.update_bufs(&self.const_buf, self.symbol_buf.borrow(), &self.node_buf);
305
306        Ok(Some(node))
307    }
308}
flussab_btor2/parser.rs

flussab_btor2/
parser.rs
