upgrade dependencies and rust edition

ekiwi · ekiwi · commit 13ddc0db58cc · 2025-08-26T12:58:18.000-04:00
diff --git a/Cargo.toml b/Cargo.toml
@@ -3,16 +3,16 @@ resolver = "2"
 members = ["patronus", "patronus-egraphs", "patronus-dse", "tools/bmc", "tools/egraphs-cond-synth", "tools/sim", "tools/simplify", "tools/view"]
 
 [workspace.package]
-edition = "2021"
+edition = "2024"
 authors = ["Kevin Laeufer <laeufer@berkeley.edu>"]
 repository = "https://github.com/cucapra/patronus"
 readme = "Readme.md"
 license = "BSD-3-Clause"
-rust-version = "1.73.0"
+rust-version = "1.85.0"
 
 [workspace.dependencies]
 rustc-hash = "2.x"
-baa = { version = "0.16.9", features = ["rand1"] }
+baa = { version = "0.17.1", features = ["rand1"] }
 egg = "0.9.5"
 regex = "1.11.1"
 boolean_expression = "0.4.4"
diff --git a/patronus-dse/src/value_summary.rs b/patronus-dse/src/value_summary.rs
@@ -2,7 +2,7 @@
 // released under BSD 3-Clause License
 // author: Kevin Laeufer <laeufer@cornell.edu>
 
-use boolean_expression::{BDDFunc, BDD};
+use boolean_expression::{BDD, BDDFunc};
 use patronus::expr::*;
 use rustc_hash::{FxBuildHasher, FxHashMap, FxHashSet};
 use std::hash::Hash;
diff --git a/patronus-egraphs/src/arithmetic.rs b/patronus-egraphs/src/arithmetic.rs
@@ -3,9 +3,9 @@
 // author: Kevin Laeufer <laeufer@cornell.edu>
 
 use baa::BitVecOps;
-use egg::{define_language, Analysis, DidMerge, Id, Language, RecExpr};
+use egg::{Analysis, DidMerge, Id, Language, RecExpr, define_language};
 use patronus::expr::*;
-use std::cmp::{max, Ordering};
+use std::cmp::{Ordering, max};
 use std::fmt::{Display, Formatter};
 use std::str::FromStr;
 
diff --git a/patronus-egraphs/src/dot.rs b/patronus-egraphs/src/dot.rs
@@ -3,7 +3,7 @@
 // author: Kevin Laeufer <laeufer@cornell.edu>
 // some of the code is based on `egg` source code which is licenced under MIT
 
-use crate::{get_const_width_or_sign, is_bin_op, EGraph};
+use crate::{EGraph, get_const_width_or_sign, is_bin_op};
 use egg::Language;
 use rustc_hash::FxHashMap;
 use std::io::{BufWriter, Write};
diff --git a/patronus-egraphs/src/rewrites.rs b/patronus-egraphs/src/rewrites.rs
@@ -10,7 +10,7 @@ introspect them in order to check re-write conditions or debug matches.
 !*/
 
 use crate::arithmetic::{eval_width_left_shift, eval_width_max_plus_1};
-use crate::{get_const_width_or_sign, is_bin_op, Arith, EGraph, WidthConstantFold};
+use crate::{Arith, EGraph, WidthConstantFold, get_const_width_or_sign, is_bin_op};
 use egg::{
     ConditionalApplier, ENodeOrVar, Id, Language, Pattern, PatternAst, Searcher, Subst, Var,
 };
@@ -22,16 +22,12 @@ macro_rules! arith_rewrite {
     (
         $name:expr;
         $lhs:expr => $rhs:expr
-    ) => {{
-        ArithRewrite::new::<&str>($name, $lhs, $rhs, [], None)
-    }};
+    ) => {{ ArithRewrite::new::<&str>($name, $lhs, $rhs, [], None) }};
     (
         $name:expr;
         $lhs:expr => $rhs:expr;
         if $vars:expr, $cond:expr
-    ) => {{
-        ArithRewrite::new($name, $lhs, $rhs, $vars, Some($cond))
-    }};
+    ) => {{ ArithRewrite::new($name, $lhs, $rhs, $vars, Some($cond)) }};
 }
 
 /// Generate our ROVER inspired rewrite rules.
@@ -162,12 +158,14 @@ impl ArithRewrite {
             };
             vec![Rewrite::new(self.name.clone(), self.lhs.clone(), cond_app).unwrap()]
         } else {
-            vec![Rewrite::new(
-                self.name.clone(),
-                self.lhs.clone(),
-                self.rhs_derived.clone(),
-            )
-            .unwrap()]
+            vec![
+                Rewrite::new(
+                    self.name.clone(),
+                    self.lhs.clone(),
+                    self.rhs_derived.clone(),
+                )
+                .unwrap(),
+            ]
         }
     }
 
diff --git a/patronus/Cargo.toml b/patronus/Cargo.toml
@@ -16,7 +16,7 @@ indexmap = "2.7.0"
 codespan-reporting = "0.11.1"
 lazy_static = "1.4.0"
 smallvec = { version = "1.x", features = ["union"] }
-rand = { version = "0.8.5", features = ["small_rng"] }
+rand = { version = "0.9", features = ["small_rng"] }
 boolean_expression.workspace = true
 regex.workspace = true
 baa.workspace = true
diff --git a/patronus/src/btor2.rs b/patronus/src/btor2.rs
@@ -6,7 +6,7 @@ mod serialize;
 mod witness;
 
 pub use parse::{
-    parse_file, parse_file_with_ctx, parse_str, DEFAULT_INPUT_PREFIX, DEFAULT_STATE_PREFIX,
+    DEFAULT_INPUT_PREFIX, DEFAULT_STATE_PREFIX, parse_file, parse_file_with_ctx, parse_str,
 };
 pub use serialize::{serialize, serialize_to_str};
 pub use witness::{parse_witness, parse_witnesses, print_witness, witness_to_string};
diff --git a/patronus/src/btor2/parse.rs b/patronus/src/btor2/parse.rs
@@ -911,11 +911,10 @@ fn report_errors(errors: Errors, name: &str, source: &str) {
 fn report_error(error: ParserError, file: &codespan_reporting::files::SimpleFile<&str, &str>) {
     let diagnostic = codespan_reporting::diagnostic::Diagnostic::error()
         .with_message(error.msg)
-        .with_labels(vec![codespan_reporting::diagnostic::Label::primary(
-            (),
-            error.start..error.end,
-        )
-        .with_message(error.explain)]);
+        .with_labels(vec![
+            codespan_reporting::diagnostic::Label::primary((), error.start..error.end)
+                .with_message(error.explain),
+        ]);
     let writer = codespan_reporting::term::termcolor::StandardStream::stderr(
         codespan_reporting::term::termcolor::ColorChoice::Auto,
     );
diff --git a/patronus/src/expr.rs b/patronus/src/expr.rs
@@ -14,18 +14,18 @@ pub mod traversal;
 mod types;
 
 pub use context::{Builder, Context, ExprRef, StringRef};
-pub use eval::{eval_array_expr, eval_bv_expr, eval_expr, SymbolValueStore};
+pub use eval::{SymbolValueStore, eval_array_expr, eval_bv_expr, eval_expr};
 pub use foreach::ForEachChild;
 pub use meta::{
-    get_fixed_point, DenseExprMetaData, DenseExprSet, ExprMap, ExprSet, SparseExprMap,
-    SparseExprSet,
+    DenseExprMetaData, DenseExprSet, ExprMap, ExprSet, SparseExprMap, SparseExprSet,
+    get_fixed_point,
 };
 pub use nodes::{ArrayType, BVLitValue, Expr, Type, WidthInt};
 pub use parse::parse_expr;
 pub use serialize::SerializableIrNode;
 pub(crate) use serialize::{serialize_expr, serialize_expr_ref};
 pub(crate) use simplify::simplify;
-pub use simplify::{simplify_single_expression, Simplifier};
+pub use simplify::{Simplifier, simplify_single_expression};
 pub use transform::simple_transform_expr;
-pub(crate) use transform::{do_transform_expr, ExprTransformMode};
+pub(crate) use transform::{ExprTransformMode, do_transform_expr};
 pub use types::{TypeCheck, TypeCheckError};
diff --git a/patronus/src/expr/context.rs b/patronus/src/expr/context.rs
@@ -14,8 +14,8 @@
 //! are no checks to ensure that a [`ExprRef`] or [`StringRef`] from different contexts are
 //! not matched. Thus working with more than one [`Context`] object can be dangerous.
 
-use crate::expr::nodes::*;
 use crate::expr::TypeCheck;
+use crate::expr::nodes::*;
 use baa::{
     ArrayOps, BitVecValue, BitVecValueIndex, BitVecValueRef, IndexToRef, SparseArrayValue, Value,
 };
diff --git a/patronus/src/expr/eval.rs b/patronus/src/expr/eval.rs
@@ -380,7 +380,7 @@ fn eval_expr_internal(
 
 #[cfg(test)]
 mod tests {
-    use super::{eval_array_expr, eval_bv_expr, SymbolValueStore};
+    use super::{SymbolValueStore, eval_array_expr, eval_bv_expr};
     use crate::expr::*;
     use baa::*;
 
@@ -395,12 +395,14 @@ mod tests {
         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::new_false()), (b, BitVecValue::new_false())].as_slice(),
-            expr
-        )
-        .is_false());
+        assert!(
+            eval_bv_expr(
+                &c,
+                [(a, BitVecValue::new_false()), (b, BitVecValue::new_false())].as_slice(),
+                expr
+            )
+            .is_false()
+        );
 
         // arithmetic and ite
         let a = c.bv_symbol("a", 128);
diff --git a/patronus/src/expr/nodes.rs b/patronus/src/expr/nodes.rs
@@ -3,8 +3,8 @@
 // released under BSD 3-Clause License
 // author: Kevin Laeufer <laeufer@cornell.edu>
 
-use crate::expr::context::{ExprRef, StringRef};
 use crate::expr::Context;
+use crate::expr::context::{ExprRef, StringRef};
 use baa::{BitVecValueIndex, BitVecValueRef};
 use std::fmt::Debug;
 
diff --git a/patronus/src/expr/simplify.rs b/patronus/src/expr/simplify.rs
@@ -4,13 +4,13 @@
 // author: Kevin Laeufer <laeufer@cornell.edu>
 
 use super::{
-    do_transform_expr, BVLitValue, Context, Expr, ExprMap, ExprRef, SparseExprMap, TypeCheck,
-    WidthInt,
+    BVLitValue, Context, Expr, ExprMap, ExprRef, SparseExprMap, TypeCheck, WidthInt,
+    do_transform_expr,
 };
 use crate::expr::meta::get_fixed_point;
 use crate::expr::transform::ExprTransformMode;
 use baa::BitVecOps;
-use smallvec::{smallvec, SmallVec};
+use smallvec::{SmallVec, smallvec};
 
 /// Applies simplifications to a single expression.
 pub fn simplify_single_expression(ctx: &mut Context, expr: ExprRef) -> ExprRef {
diff --git a/patronus/src/expr/types.rs b/patronus/src/expr/types.rs
@@ -154,9 +154,17 @@ impl TypeCheck for Expr {
             Expr::BVSlice { e, hi, lo } => {
                 let e_width = e.get_type(ctx).expect_bv("slicing")?;
                 if hi >= e_width {
-                    Err(TypeCheckError{msg: format!("Bit-slice upper index must be smaller than the width {e_width}. Not: {hi}")})
+                    Err(TypeCheckError {
+                        msg: format!(
+                            "Bit-slice upper index must be smaller than the width {e_width}. Not: {hi}"
+                        ),
+                    })
                 } else if hi < lo {
-                    Err(TypeCheckError{msg: format!("Bit-slice upper index must be larger or the same as the lower index. But {hi} < {lo}")})
+                    Err(TypeCheckError {
+                        msg: format!(
+                            "Bit-slice upper index must be larger or the same as the lower index. But {hi} < {lo}"
+                        ),
+                    })
                 } else {
                     Ok(Type::BV(hi - lo + 1))
                 }
diff --git a/patronus/src/mc.rs b/patronus/src/mc.rs
@@ -6,7 +6,7 @@ mod smt;
 mod types;
 
 pub use smt::{
-    check_assuming, check_assuming_end, get_smt_value, ModelCheckResult, SmtModelChecker,
-    SmtModelCheckerOptions, TransitionSystemEncoding, UnrollSmtEncoding,
+    ModelCheckResult, SmtModelChecker, SmtModelCheckerOptions, TransitionSystemEncoding,
+    UnrollSmtEncoding, check_assuming, check_assuming_end, get_smt_value,
 };
 pub use types::{InitValue, Witness};
diff --git a/patronus/src/mc/smt.rs b/patronus/src/mc/smt.rs
@@ -4,10 +4,10 @@
 // author: Kevin Laeufer <laeufer@cornell.edu>
 
 use crate::expr::*;
-use crate::mc::types::InitValue;
 use crate::mc::Witness;
+use crate::mc::types::InitValue;
 use crate::smt::*;
-use crate::system::analysis::{analyze_for_serialization, count_expr_uses, UseCountInt, Uses};
+use crate::system::analysis::{UseCountInt, Uses, analyze_for_serialization, count_expr_uses};
 use crate::system::{State, TransitionSystem};
 use baa::*;
 use rustc_hash::FxHashSet;
diff --git a/patronus/src/sim/interface.rs b/patronus/src/sim/interface.rs
@@ -4,8 +4,8 @@
 
 use crate::expr::{ArrayType, ExprRef, Type};
 use baa::{ArrayValue, BitVecValue, BitVecValueRef, Value};
-use rand::rngs::SmallRng;
 use rand::SeedableRng;
+use rand::rngs::SmallRng;
 
 #[derive(Debug, Copy, Clone, Eq, PartialEq, Hash)]
 pub enum InitKind {
@@ -51,7 +51,7 @@ impl InitValueGenerator {
         }
     }
 
-    pub fn gen(&mut self, tpe: Type) -> Value {
+    pub fn generate(&mut self, tpe: Type) -> Value {
         match tpe {
             Type::BV(bits) => {
                 if let Some(rng) = &mut self.rng {
diff --git a/patronus/src/sim/interpreter.rs b/patronus/src/sim/interpreter.rs
@@ -87,10 +87,10 @@ fn init_signal(
     ctx: &Context,
     state: &mut SymbolValueStore,
     symbol: ExprRef,
-    gen: &mut InitValueGenerator,
+    generator: &mut InitValueGenerator,
 ) {
     let tpe = ctx[symbol].get_type(ctx);
-    match gen.gen(tpe) {
+    match generator.generate(tpe) {
         Value::Array(value) => {
             state.define_array(symbol, value);
         }
@@ -104,16 +104,16 @@ impl Simulator for Interpreter {
     type SnapshotId = u32;
 
     fn init(&mut self, kind: InitKind) {
-        let mut gen = InitValueGenerator::from_kind(kind);
+        let mut generator = InitValueGenerator::from_kind(kind);
 
         self.data.clear();
 
         // allocate space for inputs, and states
         for state in self.sys.states.iter() {
-            init_signal(&self.ctx, &mut self.data, state.symbol, &mut gen);
+            init_signal(&self.ctx, &mut self.data, state.symbol, &mut generator);
         }
         for &symbol in self.sys.inputs.iter() {
-            init_signal(&self.ctx, &mut self.data, symbol, &mut gen);
+            init_signal(&self.ctx, &mut self.data, symbol, &mut generator);
         }
 
         // evaluate init expressions
diff --git a/patronus/src/smt/parser.rs b/patronus/src/smt/parser.rs
@@ -298,7 +298,7 @@ pub fn parse_command(ctx: &mut Context, st: &SymbolTable, input: &[u8]) -> Resul
                 return Err(SmtParserError::UnknownCommand(format!(
                     "{}",
                     String::from_utf8_lossy(name)
-                )))
+                )));
             }
         },
         _ => return Err(SmtParserError::ExpectedCommand(format!("{cmd_token:?}"))),
@@ -493,12 +493,14 @@ fn parse_pattern<'a>(
         // Types
         ///////////////////////////////////////////////////////////////////////////////////////////
         [Sym(b"_"), Sym(b"BitVec"), Sym(width)] => PType(Type::BV(parse_width(width)?)),
-        [Sym(b"Array"), PType(Type::BV(index_width)), PType(Type::BV(data_width))] => {
-            PType(Type::Array(ArrayType {
-                index_width: *index_width,
-                data_width: *data_width,
-            }))
-        }
+        [
+            Sym(b"Array"),
+            PType(Type::BV(index_width)),
+            PType(Type::BV(data_width)),
+        ] => PType(Type::Array(ArrayType {
+            index_width: *index_width,
+            data_width: *data_width,
+        })),
 
         ///////////////////////////////////////////////////////////////////////////////////////////
         // Parameterized Ops
diff --git a/patronus/src/smt/solver.rs b/patronus/src/smt/solver.rs
@@ -3,7 +3,7 @@
 // author: Kevin Laeufer <laeufer@cornell.edu>
 
 use crate::expr::{Context, ExprRef};
-use crate::smt::parser::{parse_get_value_response, SmtParserError};
+use crate::smt::parser::{SmtParserError, parse_get_value_response};
 use crate::smt::serialize::serialize_cmd;
 use std::io::{BufRead, BufReader, BufWriter};
 use std::io::{Read, Write};
diff --git a/patronus/src/system/serialize.rs b/patronus/src/system/serialize.rs
@@ -3,11 +3,11 @@
 // released under BSD 3-Clause License
 // author: Kevin Laeufer <laeufer@cornell.edu>
 
-use super::analysis::{analyze_for_serialization, SerializeSignalKind};
 use super::TransitionSystem;
+use super::analysis::{SerializeSignalKind, analyze_for_serialization};
 use crate::expr::{
-    serialize_expr, serialize_expr_ref, Context, ExprRef, SerializableIrNode, SparseExprMap,
-    TypeCheck,
+    Context, ExprRef, SerializableIrNode, SparseExprMap, TypeCheck, serialize_expr,
+    serialize_expr_ref,
 };
 use std::io::Write;
 
diff --git a/patronus/tests/simplify.rs b/patronus/tests/simplify.rs
@@ -477,8 +477,8 @@ fn test_random_z3_issue_simplification() {
     // it is nice to see that z3 implements some bit-mask support similar to ours
     // we currently do slightly better by simplifying away the right shift by a constant
     ts(
-      "or(shift_left(and(V : bv<32>, 32'd65535), 32'd17), shift_right(and(V, 32'd65535), 32'd15))",
-      "or(concat(V:bv<32>[14:0], 17'x00000), concat(31'x00000000, V[15]))"
+        "or(shift_left(and(V : bv<32>, 32'd65535), 32'd17), shift_right(and(V, 32'd65535), 32'd15))",
+        "or(concat(V:bv<32>[14:0], 17'x00000), concat(31'x00000000, V[15]))",
     );
 }
 
diff --git a/tools/egraphs-cond-synth/src/features.rs b/tools/egraphs-cond-synth/src/features.rs
@@ -2,7 +2,7 @@
 // released under BSD 3-Clause License
 // author: Kevin Laeufer <laeufer@cornell.edu>
 
-use crate::samples::{get_var_name, RuleInfo, Samples};
+use crate::samples::{RuleInfo, Samples, get_var_name};
 use bitvec::prelude as bv;
 use egg::Var;
 use patronus::expr::WidthInt;
diff --git a/tools/egraphs-cond-synth/src/main.rs b/tools/egraphs-cond-synth/src/main.rs
diff --git a/tools/egraphs-cond-synth/src/samples.rs b/tools/egraphs-cond-synth/src/samples.rs
diff --git a/tools/sim/src/main.rs b/tools/sim/src/main.rs
diff --git a/tools/simplify/src/main.rs b/tools/simplify/src/main.rs
