upgrade baa

Cargo.toml

@@ -12,7 +12,7 @@ rust-version = "1.73.0"
 
 [workspace.dependencies]
 rustc-hash = "2.x"
-baa = "0.14.7"
+baa = "0.16.0"
 egg = "0.9.5"
 regex = "1.11.1"
 boolean_expression = "0.4.4"

patronus-dse/src/engine.rs

@@ -7,6 +7,7 @@ use patronus::system::TransitionSystem;
 
 /// Symbolic execution engine.
 pub struct SymEngine {
+    #[allow(dead_code)]
     sys: TransitionSystem,
 }
 

patronus-dse/src/value_summary.rs

@@ -21,10 +21,10 @@ impl Default for GuardCtx {
 }
 
 impl GuardCtx {
-    pub fn tru(&mut self) -> Guard {
+    pub fn get_true(&mut self) -> Guard {
         self.bdd.constant(true)
     }
-    pub fn fals(&mut self) -> Guard {
+    pub fn get_false(&mut self) -> Guard {
         self.bdd.constant(false)
     }
 
@@ -110,7 +110,7 @@ impl<V: Value> ValueSummary<V> {
     pub fn new(gc: &mut GuardCtx, value: V) -> Self {
         Self {
             entries: vec![Entry {
-                guard: gc.tru(),
+                guard: gc.get_true(),
                 value,
             }],
         }
@@ -286,7 +286,7 @@ impl<V: Value + ToGuard> ValueSummary<V> {
     /// Converts the value summary into a guard.
     fn to_guard(&self, ec: &mut V::Context, gc: &mut GuardCtx) -> (Guard, Vec<Entry<V>>) {
         let mut results = vec![];
-        let mut guard = gc.fals();
+        let mut guard = gc.get_false();
         for e in self.entries.iter() {
             match e.value.to_guard(ec, gc) {
                 GuardResult::Guard(value_as_guard) => {
@@ -318,15 +318,15 @@ impl<V: Value + ToGuard> ValueSummary<V> {
         if gc.is_true(value_as_guard) {
             debug_assert!(others.is_empty());
             self.entries = vec![Entry {
-                guard: gc.tru(),
+                guard: gc.get_true(),
                 value: V::true_value(ec),
             }];
             return;
         }
         if gc.is_false(value_as_guard) {
             debug_assert!(others.is_empty());
             self.entries = vec![Entry {
-                guard: gc.tru(),
+                guard: gc.get_true(),
                 value: V::false_value(ec),
             }];
             return;
@@ -409,11 +409,11 @@ impl ToGuard for ExprRef {
         GuardResult::Guard(guard)
     }
     fn true_value(ec: &mut Self::Context) -> Self {
-        ec.tru()
+        ec.get_true()
     }
 
     fn false_value(ec: &mut Self::Context) -> Self {
-        ec.fals()
+        ec.get_false()
     }
 }
 

patronus/Cargo.toml

@@ -1,6 +1,6 @@
 [package]
 name = "patronus"
-version = "0.31.0"
+version = "0.32.0"
 description = "Hardware bug-finding toolkit."
 homepage = "https://kevinlaeufer.com"
 keywords = ["RTL", "btor", "model-checking", "SMT", "bit-vector"]

patronus/src/expr/context.rs

@@ -74,8 +74,8 @@ pub struct Context {
     exprs: indexmap::IndexSet<Expr, FxBuildHasher>,
     values: baa::ValueInterner,
     // cached special values
-    tru_expr_ref: ExprRef,
-    fals_expr_ref: ExprRef,
+    true_expr_ref: ExprRef,
+    false_expr_ref: ExprRef,
 }
 
 impl Default for Context {
@@ -85,12 +85,12 @@ impl Default for Context {
             strings: Default::default(),
             exprs: Default::default(),
             values: Default::default(),
-            tru_expr_ref: ExprRef::from_index(0),
-            fals_expr_ref: ExprRef::from_index(0),
+            true_expr_ref: ExprRef::from_index(0),
+            false_expr_ref: ExprRef::from_index(0),
         };
         // create valid cached expressions
-        out.fals_expr_ref = out.zero(1);
-        out.tru_expr_ref = out.one(1);
+        out.false_expr_ref = out.zero(1);
+        out.true_expr_ref = out.one(1);
         out
     }
 }
@@ -196,12 +196,12 @@ impl Context {
         self.array_const(data, tpe.index_width)
     }
 
-    pub fn tru(&self) -> ExprRef {
-        self.tru_expr_ref
+    pub fn get_true(&self) -> ExprRef {
+        self.true_expr_ref
     }
 
-    pub fn fals(&self) -> ExprRef {
-        self.fals_expr_ref
+    pub fn get_false(&self) -> ExprRef {
+        self.false_expr_ref
     }
 
     pub fn one(&mut self, width: WidthInt) -> ExprRef {
@@ -422,12 +422,12 @@ impl<'a> Builder<'a> {
         self.ctx.borrow_mut().zero(width)
     }
 
-    pub fn tru(&self) -> ExprRef {
-        self.ctx.borrow().tru()
+    pub fn get_true(&self) -> ExprRef {
+        self.ctx.borrow().get_true()
     }
 
-    pub fn fals(&self) -> ExprRef {
-        self.ctx.borrow().fals()
+    pub fn get_false(&self) -> ExprRef {
+        self.ctx.borrow().get_false()
     }
 
     pub fn zero_array(&self, tpe: ArrayType) -> ExprRef {
@@ -558,8 +558,8 @@ mod tests {
         let mut ctx = Context::default();
 
         // ids 1 and 2 are reserved for true and false
-        assert_eq!(ctx.fals().0.get(), 1);
-        assert_eq!(ctx.tru().0.get(), 2);
+        assert_eq!(ctx.get_false().0.get(), 1);
+        assert_eq!(ctx.get_true().0.get(), 2);
 
         let str_id0 = ctx.string("a".into());
         let id0 = ctx.add_expr(Expr::BVSymbol {

patronus/src/expr/eval.rs

@@ -391,16 +391,16 @@ mod tests {
         // boolean
         let a = c.bv_symbol("a", 1);
         let a_and_1 = c.build(|c| c.and(a, c.one(1)));
-        assert!(eval_bv_expr(&c, [(a, BitVecValue::tru())].as_slice(), a_and_1).is_tru());
-        assert!(eval_bv_expr(&c, [(a, BitVecValue::fals())].as_slice(), a_and_1).is_fals());
+        assert!(eval_bv_expr(&c, [(a, BitVecValue::new_true())].as_slice(), a_and_1).is_true());
+        assert!(eval_bv_expr(&c, [(a, BitVecValue::new_false())].as_slice(), a_and_1).is_false());
         let b = c.bv_symbol("b", 1);
         let expr = c.build(|c| c.or(c.and(a, c.not(b)), c.and(a, b)));
         assert!(eval_bv_expr(
             &c,
-            [(a, BitVecValue::fals()), (b, BitVecValue::fals())].as_slice(),
+            [(a, BitVecValue::new_false()), (b, BitVecValue::new_false())].as_slice(),
             expr
         )
-        .is_fals());
+        .is_false());
 
         // arithmetic and ite
         let a = c.bv_symbol("a", 128);

patronus/src/expr/parse.rs

@@ -107,10 +107,10 @@ impl<'a> Parser<'a> {
         } else if let Some(c) = TRUE_FALSE_REGEX.captures(self.inp) {
             self.consume_c(&c);
             if c.get(2).is_some() {
-                Some(self.ctx.tru())
+                Some(self.ctx.get_true())
             } else {
                 debug_assert!(c.get(3).is_some());
-                Some(self.ctx.fals())
+                Some(self.ctx.get_false())
             }
         } else {
             None
@@ -376,7 +376,7 @@ mod tests {
 
         assert_eq!(
             parse_expr(&mut ctx, "and(true, false)"),
-            ctx.build(|c| c.and(c.tru(), c.fals()))
+            ctx.build(|c| c.and(c.get_true(), c.get_false()))
         );
 
         assert_eq!(
@@ -396,11 +396,11 @@ mod tests {
         // nested functions
         assert_eq!(
             parse_expr(&mut ctx, "or(and(true, true), false)"),
-            ctx.build(|c| c.or(c.and(c.tru(), c.tru()), c.fals()))
+            ctx.build(|c| c.or(c.and(c.get_true(), c.get_true()), c.get_false()))
         );
         assert_eq!(
             parse_expr(&mut ctx, "or(false, and(true, true))"),
-            ctx.build(|c| c.or(c.fals(), c.and(c.tru(), c.tru())))
+            ctx.build(|c| c.or(c.get_false(), c.and(c.get_true(), c.get_true())))
         );
     }
 }

patronus/src/expr/simplify.rs

@@ -72,7 +72,7 @@ fn simplify_ite(ctx: &mut Context, cond: ExprRef, tru: ExprRef, fals: ExprRef) -
 
     // constant condition
     if let Expr::BVLiteral(value) = ctx[cond] {
-        if value.get(ctx).is_fals() {
+        if value.get(ctx).is_false() {
             // ite(false, a, b) -> b
             return Some(fals);
         } else {
@@ -154,14 +154,14 @@ fn find_one_concat(ctx: &Context, a: ExprRef, b: ExprRef) -> Option<(ExprRef, Ex
 fn simplify_bv_equal(ctx: &mut Context, a: ExprRef, b: ExprRef) -> Option<ExprRef> {
     // a == a -> true
     if a == b {
-        return Some(ctx.tru());
+        return Some(ctx.get_true());
     }
 
     match find_lits_commutative(ctx, a, b) {
         Lits::Two(va, vb) => {
             // two values that are the same should always be hash-consed to the same ExprRef
             debug_assert!(!va.get(ctx).is_equal(&vb.get(ctx)));
-            return Some(ctx.fals());
+            return Some(ctx.get_false());
         }
         Lits::One((lit, _), expr) => {
             if lit.is_true() {

patronus/src/smt/parser.rs

@@ -607,8 +607,8 @@ fn early_parse_single_token<'a>(
                 "decimal constant: {}",
                 String::from_utf8_lossy(value)
             ))),
-            3 => Ok(ParserItem::PExpr(ctx.tru())),
-            4 => Ok(ParserItem::PExpr(ctx.fals())),
+            3 => Ok(ParserItem::PExpr(ctx.get_true())),
+            4 => Ok(ParserItem::PExpr(ctx.get_false())),
             _ => unreachable!("not part of the regex!"),
         }
     } else {

patronus/src/smt/serialize.rs

@@ -41,10 +41,10 @@ pub fn serialize_expr(out: &mut impl Write, ctx: &Context, expr: ExprRef) -> Res
                     let value = v.get(ctx);
                     if value.width() > 1 {
                         write!(out, "#b{}", v.get(ctx).to_bit_str())?;
-                    } else if value.is_tru() {
+                    } else if value.is_true() {
                         write!(out, "true")?;
                     } else {
-                        debug_assert!(value.is_fals());
+                        debug_assert!(value.is_false());
                         write!(out, "false")?;
                     }
                 }
@@ -482,8 +482,8 @@ mod tests {
         let mut ctx = Context::default();
         let a = ctx.bv_symbol("a", 2);
         assert_eq!(s_expr(&ctx, a), "a");
-        assert_eq!(s_expr(&ctx, ctx.fals()), "false");
-        assert_eq!(s_expr(&ctx, ctx.tru()), "true");
+        assert_eq!(s_expr(&ctx, ctx.get_false()), "false");
+        assert_eq!(s_expr(&ctx, ctx.get_true()), "true");
         let bv_lit = ctx.bit_vec_val(3, 3);
         assert_eq!(s_expr(&ctx, bv_lit), "#b011");
     }