Add an IR for BTOR2 to reduce the dependencies on the C parser #2003
Conversation
There was a problem hiding this comment.
Left a bunch of nits here and there. It has been a while since I used turnt but it doesn't seem like there are .out files for the tests. Were those omitted by mistake? Are we not at that stage yet? Or am I just missing something?
In any case, good work! Very exciting
tools/btor2/btor2i/.gitignore
Outdated
There was a problem hiding this comment.
This gitignore file shouldn't be committed. If there's anything not being ignored that should be, please add it to the main gitignore
tools/btor2/btor2i/src/interp.rs
Outdated
| use crate::ir::BinOpType; | ||
| use crate::ir::Btor2Instr; | ||
| use crate::ir::Btor2InstrContents; | ||
| use crate::ir::ConstantType; | ||
| use crate::ir::LiteralType; | ||
| use crate::ir::SortType; | ||
| use crate::ir::UnOpType; |
There was a problem hiding this comment.
style nit: All these imports can be merged together
tools/btor2/btor2i/src/interp.rs
Outdated
| arg2: _, | ||
| kind, | ||
| } => match kind { | ||
| BinOpType::Add => eval_binary_op(env, line, SharedEnvironment::add), |
There was a problem hiding this comment.
style nit: if the args are not needed in the match they can be elided like so
| BinOpType::Add => eval_binary_op(env, line, SharedEnvironment::add), | |
| Btor2InstrContents::BinOp { kind, .. } => match kind { |
There was a problem hiding this comment.
ugh it applied on the wrong line, but you get the point
tools/btor2/btor2i/src/interp.rs
Outdated
| arg2: _, | ||
| kind, | ||
| } => match kind { | ||
| BinOpType::Add => eval_binary_op(env, line, SharedEnvironment::add), |
There was a problem hiding this comment.
The structure of these matches could be further simplified into a single arm
which just calls eval_binary_op and selects the appropriate function with a
helper function that takes kind as an argument. The helper function can match
on kind and this function will no longer need to which should make things easier
to follow.
tools/btor2/btor2i/src/interp.rs
Outdated
| // binary - boolean | ||
| btor2tools::Btor2Tag::Iff => { | ||
| eval_binary_op(env, line, SharedEnvironment::iff) | ||
| prog_iterator.try_for_each(|line| match &line.contents { |
There was a problem hiding this comment.
I don't see a strong reason to use try_for_each here since it would do the
same thing as a for loop with use of the ? operator and the latter is, in my
subjective opinion, easier to read
tools/btor2/btor2i/src/ir.rs
Outdated
| Constant { | ||
| constant: Option<String>, | ||
| kind: ConstantType, | ||
| }, | ||
| Literal { | ||
| kind: LiteralType, | ||
| }, | ||
| UnOp { | ||
| arg1: i64, | ||
| kind: UnOpType, | ||
| }, | ||
| BinOp { | ||
| arg1: i64, | ||
| arg2: i64, | ||
| kind: BinOpType, | ||
| }, | ||
| Conditional { | ||
| arg1: i64, | ||
| arg2: i64, | ||
| arg3: i64, | ||
| }, | ||
| Slice { | ||
| arg1: i64, | ||
| u: i64, | ||
| l: i64, | ||
| }, | ||
| Input { | ||
| name: String, | ||
| }, | ||
| Output { | ||
| name: String, | ||
| arg1: i64, | ||
| }, |
There was a problem hiding this comment.
I would double-check if i64 is the correct choice for all these arguments. Is
it the case that negative values are possible?
|
|
||
| pub enum Btor2InstrContents { | ||
| Constant { | ||
| constant: Option<String>, |
There was a problem hiding this comment.
In the future it might be better if this String is parsed into something, but
for now this is fine
tools/btor2/btor2i/src/ir.rs
Outdated
| btor2tools::Btor2Tag::Not => convert_unary_op(line), | ||
| btor2tools::Btor2Tag::Inc => convert_unary_op(line), | ||
| btor2tools::Btor2Tag::Dec => convert_unary_op(line), | ||
| btor2tools::Btor2Tag::Neg => convert_unary_op(line), | ||
| btor2tools::Btor2Tag::Redand => convert_unary_op(line), | ||
| btor2tools::Btor2Tag::Redor => convert_unary_op(line), | ||
| btor2tools::Btor2Tag::Redxor => convert_unary_op(line), |
There was a problem hiding this comment.
These arms can all be collapsed into a single pattern match, i.e. the or | of
the possible patterns. This is true of several other sections. It's not critical
but I think it is slightly cleaner
tools/btor2/btor2i/src/main.rs
Outdated
| line.symbol().unwrap().to_string_lossy().into_owned(); | ||
| let src_node_idx = line.args()[0] as usize; | ||
| let output_val = s_env.get(src_node_idx); | ||
| ir_lines.iter().for_each(|line| { |
There was a problem hiding this comment.
I don't see a strong reason to use for_each here over a normal for loop
tools/btor2/btor2i/src/values.rs
Outdated
| use crate::bvec::BitVector; | ||
|
|
||
| impl From<list<bool>> for BitVector { | ||
|
|
||
| } | ||
|
|
||
| impl From<u8> for BitVector { | ||
|
|
||
| } | ||
|
|
||
| impl From<u16> for BitVector { | ||
|
|
||
| } | ||
|
|
||
| impl From<u32> for BitVector { | ||
|
|
||
| } | ||
|
|
||
| impl From<u64> for BitVector { | ||
|
|
||
| } | ||
|
|
||
| impl From<u128> for BitVector { | ||
|
|
||
| } | ||
|
|
||
| impl From<usize> for BitVector { | ||
|
|
||
| } |
There was a problem hiding this comment.
This file isn't in the module tree and so can be deleted for the moment
Modify the BTOR2 interpreter to use a new IR that does not depend on the BTOR2 parser written in C. I also added a suite of test BTOR2 programs to ensure that the interpreter remained correct with the new IR.