Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[Cider2] use baa as bit-vector library #2281

Merged
merged 7 commits into from
Sep 16, 2024
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
17 changes: 15 additions & 2 deletions Cargo.lock

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

1 change: 1 addition & 0 deletions interp/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -46,6 +46,7 @@ calyx-frontend = { path = "../calyx-frontend" }
btor2i = { path = "../tools/btor2/btor2i" }

ciborium = "0.2.2"
baa = { version = "0.6.0", features = ["bigint", "serde1", "fraction1"] }

[dev-dependencies]
proptest = "1.0.0"
Expand Down
7 changes: 7 additions & 0 deletions interp/proptest-regressions/tests/values.txt
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
# Seeds for failure cases proptest has generated in the past. It is
# automatically read and these particular cases re-run before any
# novel cases are generated.
#
# It is recommended to check this file in to source control so that
# everyone who runs the test benefits from these saved cases.
cc 8bfbc0242b84cd41283ecc9c000e88751215cf3bbef619b67f08dcb64f8ab602 # shrinks to input = 0
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

What uses this input file?

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

cargo test

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It's the regression seeds for the proptest tests

9 changes: 5 additions & 4 deletions interp/src/debugger/commands/command_parser.rs
Original file line number Diff line number Diff line change
@@ -1,6 +1,7 @@
use super::core::{
Command, ParsedBreakPointID, ParsedGroupName, PrintMode, WatchPosition,
};
use baa::WidthInt;
use pest_consume::{match_nodes, Error, Parser};

type ParseResult<T> = std::result::Result<T, Error<Rule>>;
Expand Down Expand Up @@ -87,15 +88,15 @@ impl CommandParser {
))
}

fn pc_ufx(input: Node) -> ParseResult<usize> {
fn pc_ufx(input: Node) -> ParseResult<WidthInt> {
Ok(match_nodes!(input.into_children();
[num(n)] => n as usize
[num(n)] => n as WidthInt
))
}

fn pc_sfx(input: Node) -> ParseResult<usize> {
fn pc_sfx(input: Node) -> ParseResult<WidthInt> {
Ok(match_nodes!(input.into_children();
[num(n)] => n as usize
[num(n)] => n as WidthInt
))
}

Expand Down
14 changes: 7 additions & 7 deletions interp/src/errors.rs
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@ use crate::flatten::{
},
structures::environment::Environment,
};
use crate::values::Value;
use baa::{BitVecOps, BitVecValue};
use calyx_ir::Id;
use calyx_utils::{Error as CalyxError, MultiError as CalyxMultiError};
use rustyline::error::ReadlineError;
Expand Down Expand Up @@ -136,14 +136,14 @@ pub enum InterpreterError {
/// A currently defunct error type for cross branch conflicts
#[error(
"par assignments not disjoint: {parent_id}.{port_id}
1. {v1}
2. {v2}"
1. {v1:?}
2. {v2:?}"
)]
ParOverlap {
port_id: Id,
parent_id: Id,
v1: Value,
v2: Value,
v1: BitVecValue,
v2: BitVecValue,
},

#[error("{mem_dim} Memory given initialization data with invalid dimension.
Expand Down Expand Up @@ -277,8 +277,8 @@ impl InterpreterError {
let (a1_str, a1_source) = assign_to_string(&a1, env);
let (a2_str, a2_source) = assign_to_string(&a2, env);

let a1_v = a1.val();
let a2_v = a2.val();
let a1_v = a1.val().to_bit_str();
let a2_v = a2.val().to_bit_str();
let a1_source = a1_source
.map(|(comp, s)| source_to_string(&s, comp, env))
.unwrap_or_default();
Expand Down
58 changes: 30 additions & 28 deletions interp/src/flatten/flat_ir/base.rs
Original file line number Diff line number Diff line change
Expand Up @@ -3,15 +3,14 @@ use std::{
ops::{Add, Sub},
};

use super::{cell_prototype::CellPrototype, prelude::Identifier};
use crate::{
flatten::structures::index_trait::{
impl_index, impl_index_nonzero, IndexRange, IndexRef,
},
serialization::PrintCode,
values::Value,
};

use super::{cell_prototype::CellPrototype, prelude::Identifier};
use baa::{BitVecOps, BitVecValue};

// making these all u32 for now, can give the macro an optional type as the
// second arg to contract or expand as needed
Expand Down Expand Up @@ -423,14 +422,14 @@ impl From<AssignmentIdx> for AssignmentWinner {
/// concrete value and the "winner" which assigned it.
#[derive(Clone, PartialEq)]
pub struct AssignedValue {
val: Value,
val: BitVecValue,
winner: AssignmentWinner,
}

impl std::fmt::Debug for AssignedValue {
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
f.debug_struct("AssignedValue")
.field("val", &format!("{}", &self.val))
.field("val", &self.val.to_bit_str())
.field("winner", &self.winner)
.finish()
}
Expand All @@ -445,7 +444,7 @@ impl std::fmt::Display for AssignedValue {

impl AssignedValue {
/// Creates a new AssignedValue
pub fn new<T: Into<AssignmentWinner>>(val: Value, winner: T) -> Self {
pub fn new<T: Into<AssignmentWinner>>(val: BitVecValue, winner: T) -> Self {
Self {
val,
winner: winner.into(),
Expand All @@ -458,7 +457,7 @@ impl AssignedValue {
}

/// Returns the value of the assigned value
pub fn val(&self) -> &Value {
pub fn val(&self) -> &BitVecValue {
&self.val
}

Expand All @@ -471,15 +470,15 @@ impl AssignedValue {
/// a one bit high value
pub fn implicit_bit_high() -> Self {
Self {
val: Value::bit_high(),
val: BitVecValue::tru(),
winner: AssignmentWinner::Implicit,
}
}

/// A utility constructor which returns an [`AssignedValue`] with the given
/// value and a [`AssignmentWinner::Cell`] as the winner
#[inline]
pub fn cell_value(val: Value) -> Self {
pub fn cell_value(val: BitVecValue) -> Self {
Self {
val,
winner: AssignmentWinner::Cell,
Expand All @@ -489,7 +488,7 @@ impl AssignedValue {
/// A utility constructor which returns an [`AssignedValue`] with the given
/// value and a [`AssignmentWinner::Implicit`] as the winner
#[inline]
pub fn implicit_value(val: Value) -> Self {
pub fn implicit_value(val: BitVecValue) -> Self {
Self {
val,
winner: AssignmentWinner::Implicit,
Expand All @@ -500,13 +499,13 @@ impl AssignedValue {
/// high value and a [`AssignmentWinner::Cell`] as the winner
#[inline]
pub fn cell_b_high() -> Self {
Self::cell_value(Value::bit_high())
Self::cell_value(BitVecValue::tru())
}
/// A utility constructor which returns an [`AssignedValue`] with a one bit
/// low value and a [`AssignmentWinner::Cell`] as the winner
#[inline]
pub fn cell_b_low() -> Self {
Self::cell_value(Value::bit_low())
Self::cell_value(BitVecValue::fals())
}
}

Expand Down Expand Up @@ -541,21 +540,20 @@ impl PortValue {
}

/// If the value is defined, returns the value cast to a boolean. Otherwise
/// returns `None`. It uses the [`Value::as_bool`] method and will panic if
/// the given value is not one bit wide.
/// returns `None`. It will panic if the given value is not one bit wide.
pub fn as_bool(&self) -> Option<bool> {
self.0.as_ref().map(|x| x.val().as_bool())
self.0.as_ref().map(|x| x.val().to_bool().unwrap())
}

/// If the value is defined, returns the value cast to a usize. Otherwise
/// returns `None`. It uses the [`Value::as_usize`] method.
pub fn as_usize(&self) -> Option<usize> {
self.0.as_ref().map(|x| x.val().as_usize())
/// If the value is defined, returns the value cast to a u64. Otherwise,
/// returns `None`. It uses the [`BitVecValue::to_u64`] method.
pub fn as_u64(&self) -> Option<u64> {
self.0.as_ref().map(|x| x.val().to_u64().unwrap())
}

/// Returns a reference to the underlying value if it is defined. Otherwise
/// returns `None`.
pub fn val(&self) -> Option<&Value> {
pub fn val(&self) -> Option<&BitVecValue> {
self.0.as_ref().map(|x| &x.val)
}

Expand All @@ -576,17 +574,17 @@ impl PortValue {
}

/// Creates a [PortValue] that has the "winner" as a cell
pub fn new_cell(val: Value) -> Self {
pub fn new_cell(val: BitVecValue) -> Self {
Self(Some(AssignedValue::cell_value(val)))
}

/// Creates a width-bit zero [PortValue] that has the "winner" as a cell
pub fn new_cell_zeroes(width: u32) -> Self {
Self::new_cell(Value::zeroes(width))
Self::new_cell(BitVecValue::zero(width))
}

/// Creates a [PortValue] that has the "winner" as implicit
pub fn new_implicit(val: Value) -> Self {
pub fn new_implicit(val: BitVecValue) -> Self {
Self(Some(AssignedValue::implicit_value(val)))
}

Expand All @@ -602,11 +600,15 @@ impl PortValue {
if let Some(v) = self.0.as_ref() {
let v = &v.val;
match print_code {
PrintCode::Unsigned => format!("{}", v.as_unsigned()),
PrintCode::Signed => format!("{}", v.as_signed()),
PrintCode::UFixed(num) => format!("{}", v.as_ufp(num)),
PrintCode::SFixed(num) => format!("{}", v.as_sfp(num)),
PrintCode::Binary => format!("{}", v),
PrintCode::Unsigned => format!("{}", v.to_big_uint()),
PrintCode::Signed => format!("{}", v.to_big_int()),
PrintCode::UFixed(num) => {
format!("{}", v.to_unsigned_fixed_point(num).unwrap())
}
PrintCode::SFixed(num) => {
format!("{}", v.to_signed_fixed_point(num).unwrap())
}
PrintCode::Binary => v.to_bit_str(),
}
} else {
"undef".to_string()
Expand Down
13 changes: 6 additions & 7 deletions interp/src/flatten/primitives/btor2_prim.rs
Original file line number Diff line number Diff line change
Expand Up @@ -5,8 +5,7 @@ use crate::flatten::primitives::prim_trait::{Primitive, UpdateResult};
use crate::flatten::primitives::{declare_ports, ports};
use crate::flatten::structures::environment::PortMap;

use crate::values::Value;

use baa::{BitVecValue, WidthInt};
// use std::env;

use std::cell::RefCell;
Expand All @@ -15,12 +14,12 @@ use std::collections::HashMap;
pub struct MyBtor2Add<'a> {
program: RefCell<Btor2Program<'a>>,
base_port: GlobalPortIdx,
width: usize, // do stuff
width: WidthInt, // do stuff
}

impl<'a> MyBtor2Add<'a> {
declare_ports![ LEFT:0, RIGHT:1, OUT:2 ];
pub fn new(base: GlobalPortIdx, width: usize) -> Self {
pub fn new(base: GlobalPortIdx, width: WidthInt) -> Self {
Self {
program: RefCell::new(Btor2Program::new(
"../tools/btor2/core/std_add.btor",
Expand All @@ -37,17 +36,17 @@ impl<'a> Primitive for MyBtor2Add<'a> {
let input_map = HashMap::from([
(
"left".to_string(),
port_map[left].as_usize().unwrap_or(0).to_string(),
port_map[left].as_u64().unwrap_or(0).to_string(),
),
(
"right".to_string(),
port_map[right].as_usize().unwrap_or(0).to_string(),
port_map[right].as_u64().unwrap_or(0).to_string(),
),
]);
match self.program.borrow_mut().run(input_map) {
Ok(output_map) => Ok(port_map.insert_val(
out,
AssignedValue::cell_value(Value::from(
AssignedValue::cell_value(BitVecValue::from_u64(
output_map["out"],
self.width,
)),
Expand Down
Loading
Loading