various improvements and fixes from the sca branch

Author: ekiwi

Cargo.toml

@@ -8,7 +8,7 @@ authors = ["Kevin Laeufer <laeufer@berkeley.edu>"]
 repository = "https://github.com/cucapra/patronus"
 readme = "Readme.md"
 license = "BSD-3-Clause"
-rust-version = "1.85.0"
+rust-version = "1.88.0"
 # used by main patronus library and python bindings
 version = "0.35.0"
 

patronus-egraphs/src/arithmetic.rs

@@ -282,10 +282,10 @@ fn convert_bin_op(
         width_out,
         width_a,
         sign_a,
-        converted_b,
+        converted_a,
         width_b,
         sign_b,
-        converted_a,
+        converted_b,
     ]))
 }
 

patronus/src/expr.rs

@@ -14,7 +14,7 @@ mod transform;
 pub mod traversal;
 mod types;
 
-pub use analysis::{UseCountInt, count_expr_uses, update_expr_child_uses};
+pub use analysis::{UseCountInt, count_expr_uses, find_symbols, update_expr_child_uses};
 pub use context::{Builder, Context, ExprRef, StringRef};
 pub use eval::{SymbolValueStore, eval_array_expr, eval_bv_expr, eval_expr};
 pub use foreach::ForEachChild;

patronus/src/expr/analysis.rs

@@ -3,7 +3,8 @@
 // released under BSD 3-Clause License
 // author: Kevin Laeufer <laeufer@cornell.edu>
 
-use crate::expr::{Context, ExprMap, ExprRef, ForEachChild, SparseExprMap};
+use crate::expr::{Context, ExprMap, ExprRef, ForEachChild, SparseExprMap, traversal};
+use rustc_hash::FxHashSet;
 
 pub type UseCountInt = u16;
 
@@ -24,6 +25,17 @@ pub fn count_expr_uses(ctx: &Context, roots: Vec<ExprRef>) -> impl ExprMap<UseCo
     use_count
 }
 
+/// Returns all symbols in the given expression.
+pub fn find_symbols(ctx: &Context, e: ExprRef) -> FxHashSet<ExprRef> {
+    let mut out = FxHashSet::default();
+    traversal::bottom_up(ctx, e, |ctx, e, _| {
+        if ctx[e].is_symbol() {
+            out.insert(e);
+        }
+    });
+    out
+}
+
 /// Increments the use counts for all children of the expression `expr` and
 /// adds any child encountered for the first time to the `todo` list.
 #[inline]

patronus/src/expr/context.rs

@@ -17,7 +17,8 @@
 use crate::expr::TypeCheck;
 use crate::expr::nodes::*;
 use baa::{
-    ArrayOps, BitVecValue, BitVecValueIndex, BitVecValueRef, IndexToRef, SparseArrayValue, Value,
+    ArrayOps, BitVecOps, BitVecValue, BitVecValueIndex, BitVecValueRef, IndexToRef,
+    SparseArrayValue, Value,
 };
 use rustc_hash::FxBuildHasher;
 use std::borrow::Borrow;
@@ -53,18 +54,20 @@ pub struct ExprRef(NonZeroU32);
 impl Debug for ExprRef {
     fn fmt(&self, f: &mut Formatter<'_>) -> std::fmt::Result {
         // we need a custom implementation in order to show the zero based index
-        write!(f, "ExprRef({})", self.index())
+        let index: usize = (*self).into();
+        write!(f, "ExprRef({})", index)
     }
 }
 
-impl ExprRef {
-    // TODO: reduce visibility to pub(crate)
-    pub fn from_index(index: usize) -> Self {
-        ExprRef(NonZeroU32::new((index + 1) as u32).unwrap())
+impl From<ExprRef> for usize {
+    fn from(value: ExprRef) -> Self {
+        (value.0.get() - 1) as usize
     }
+}
 
-    pub(crate) fn index(&self) -> usize {
-        (self.0.get() - 1) as usize
+impl From<usize> for ExprRef {
+    fn from(index: usize) -> Self {
+        ExprRef(NonZeroU32::new((index + 1) as u32).unwrap())
     }
 }
 
@@ -87,8 +90,8 @@ impl Default for Context {
             strings: Default::default(),
             exprs: Default::default(),
             values: Default::default(),
-            true_expr_ref: ExprRef::from_index(0),
-            false_expr_ref: ExprRef::from_index(0),
+            true_expr_ref: 0.into(),  // only a placeholder!
+            false_expr_ref: 0.into(), // only a placeholder!
         };
         // create valid cached expressions
         out.false_expr_ref = out.zero(1);
@@ -105,7 +108,7 @@ impl Context {
 
     pub(crate) fn add_expr(&mut self, value: Expr) -> ExprRef {
         let (index, _) = self.exprs.insert_full(value);
-        ExprRef::from_index(index)
+        index.into()
     }
 
     pub fn string(&mut self, value: std::borrow::Cow<str>) -> StringRef {
@@ -127,7 +130,7 @@ impl Index<ExprRef> for Context {
 
     fn index(&self, index: ExprRef) -> &Self::Output {
         self.exprs
-            .get_index(index.index())
+            .get_index(index.into())
             .expect("Invalid ExprRef!")
     }
 }
@@ -142,21 +145,15 @@ impl Index<StringRef> for Context {
     }
 }
 
+/// Convenience methods to inspect IR nodes.
 impl Context {
-    /// Returns the number of interned expressions in this context.
-    pub fn num_exprs(&self) -> usize {
-        self.exprs.len()
-    }
-
-    /// Returns a reference to the expression for the given reference.
-    /// Panics if the reference is invalid (use indices in range 0..num_exprs()).
-    pub fn get_expr(&self, r: ExprRef) -> &Expr {
-        &self[r]
-    }
-
-    /// Returns the zero-based intern index of the given expression reference.
-    pub fn expr_index(&self, r: ExprRef) -> usize {
-        r.index()
+    /// Returns whether `e` represents a bit vector literal `0` of any width.
+    pub fn is_zero(&self, e: ExprRef) -> bool {
+        if let Expr::BVLiteral(value) = self[e] {
+            value.get(self).is_zero()
+        } else {
+            false
+        }
     }
 }
 
@@ -247,6 +244,11 @@ impl Context {
     pub fn ones(&mut self, width: WidthInt) -> ExprRef {
         self.bv_lit(&BitVecValue::ones(width))
     }
+
+    pub fn distinct(&mut self, a: ExprRef, b: ExprRef) -> ExprRef {
+        let is_eq = self.equal(a, b);
+        self.not(is_eq)
+    }
     pub fn equal(&mut self, a: ExprRef, b: ExprRef) -> ExprRef {
         debug_assert_eq!(a.get_type(self), b.get_type(self));
         if a.get_type(self).is_bit_vector() {
@@ -311,6 +313,20 @@ impl Context {
         debug_assert_eq!(a.get_bv_type(self).unwrap(), b.get_bv_type(self).unwrap());
         self.add_expr(Expr::BVXor(a, b, b.get_bv_type(self).unwrap()))
     }
+
+    pub fn xor3(&mut self, a: ExprRef, b: ExprRef, c: ExprRef) -> ExprRef {
+        let x = self.xor(a, b);
+        self.xor(x, c)
+    }
+
+    pub fn majority(&mut self, a: ExprRef, b: ExprRef, c: ExprRef) -> ExprRef {
+        let a_and_b = self.and(a, b);
+        let a_and_c = self.and(a, c);
+        let b_and_c = self.and(b, c);
+        let x = self.or(a_and_b, a_and_c);
+        self.or(x, b_and_c)
+    }
+
     pub fn shift_left(&mut self, a: ExprRef, b: ExprRef) -> ExprRef {
         debug_assert_eq!(a.get_bv_type(self).unwrap(), b.get_bv_type(self).unwrap());
         self.add_expr(Expr::BVShiftLeft(a, b, b.get_bv_type(self).unwrap()))
@@ -515,6 +531,12 @@ impl<'a> Builder<'a> {
     pub fn xor(&self, a: ExprRef, b: ExprRef) -> ExprRef {
         self.ctx.borrow_mut().xor(a, b)
     }
+    pub fn xor3(&mut self, a: ExprRef, b: ExprRef, c: ExprRef) -> ExprRef {
+        self.ctx.borrow_mut().xor3(a, b, c)
+    }
+    pub fn majority(&mut self, a: ExprRef, b: ExprRef, c: ExprRef) -> ExprRef {
+        self.ctx.borrow_mut().majority(a, b, c)
+    }
     pub fn shift_left(&self, a: ExprRef, b: ExprRef) -> ExprRef {
         self.ctx.borrow_mut().shift_left(a, b)
     }

patronus/src/expr/meta.rs

@@ -109,17 +109,19 @@ impl<T: Default + Clone + Debug> Index<ExprRef> for DenseExprMetaData<T> {
 
     #[inline]
     fn index(&self, e: ExprRef) -> &Self::Output {
-        self.inner.get(e.index()).unwrap_or(&self.default)
+        let index: usize = e.into();
+        self.inner.get(index).unwrap_or(&self.default)
     }
 }
 
 impl<T: Default + Clone + Debug> IndexMut<ExprRef> for DenseExprMetaData<T> {
     #[inline]
     fn index_mut(&mut self, e: ExprRef) -> &mut Self::Output {
-        if self.inner.len() <= e.index() {
-            self.inner.resize(e.index() + 1, T::default());
+        let index: usize = e.into();
+        if self.inner.len() <= index {
+            self.inner.resize(index + 1, T::default());
         }
-        &mut self.inner[e.index()]
+        &mut self.inner[index]
     }
 }
 
@@ -155,7 +157,7 @@ impl<'a, T> Iterator for ExprMetaDataIter<'a, T> {
         match self.inner.next() {
             None => None,
             Some(value) => {
-                let index_ref = ExprRef::from_index(self.index);
+                let index_ref = self.index.into();
                 self.index += 1;
                 Some((index_ref, value))
             }
@@ -206,7 +208,7 @@ impl ExprSet for DenseExprSet {
 
 #[inline]
 fn index_to_word_and_bit(index: ExprRef) -> (usize, u32) {
-    let index = index.index();
+    let index: usize = index.into();
     let word = index / Word::BITS as usize;
     let bit = index % Word::BITS as usize;
     (word, bit as u32)
@@ -239,9 +241,9 @@ mod tests {
     #[test]
     fn test_get_fixed_point() {
         let mut m = DenseExprMetaData::default();
-        let zero = ExprRef::from_index(0);
-        let one = ExprRef::from_index(1);
-        let two = ExprRef::from_index(2);
+        let zero: ExprRef = 0usize.into();
+        let one: ExprRef = 1usize.into();
+        let two: ExprRef = 2usize.into();
         m[zero] = Some(one);
         m[one] = Some(two);
         m[two] = Some(two);
@@ -257,8 +259,9 @@ mod tests {
     #[test]
     fn test_dense_bool() {
         let mut m = DenseExprSet::default();
-        assert!(!m.contains(&ExprRef::from_index(7)));
-        m.insert(ExprRef::from_index(7));
-        assert!(m.contains(&ExprRef::from_index(7)));
+        let expr_ref_7: ExprRef = 7usize.into();
+        assert!(!m.contains(&expr_ref_7));
+        m.insert(expr_ref_7);
+        assert!(m.contains(&expr_ref_7));
     }
 }

patronus/src/expr/simplify.rs

@@ -1,14 +1,15 @@
 // Copyright 2023 The Regents of the University of California
-// Copyright 2024 Cornell University
+// Copyright 2024-2026 Cornell University
 // released under BSD 3-Clause License
 // author: Kevin Laeufer <laeufer@cornell.edu>
 
 use super::{
-    BVLitValue, Context, Expr, ExprMap, ExprRef, SparseExprMap, TypeCheck, WidthInt,
-    do_transform_expr,
+    BVLitValue, Context, Expr, ExprMap, ExprRef, SerializableIrNode, SparseExprMap, TypeCheck,
+    WidthInt, do_transform_expr, find_symbols,
 };
 use crate::expr::meta::get_fixed_point;
 use crate::expr::transform::ExprTransformMode;
+use crate::smt::{CheckSatResponse, SolverContext};
 use baa::BitVecOps;
 use smallvec::{SmallVec, smallvec};
 
@@ -38,6 +39,68 @@ impl<T: ExprMap<Option<ExprRef>>> Simplifier<T> {
         );
         get_fixed_point(&mut self.cache, e).unwrap()
     }
+
+    /// Uses an SMT solver to check all simplification steps that have been made with this Simplifier.
+    /// Returns the number of incorrect simplifications.
+    pub fn verify_simplification(
+        &self,
+        ctx: &mut Context,
+        solver: &mut impl SolverContext,
+    ) -> crate::smt::Result<usize> {
+        let mut incorrect = 0;
+        let mut correct = 0;
+        for (key, &value) in self.cache.iter() {
+            if let Some(simplified) = value {
+                let key_symbols = find_symbols(ctx, key);
+                let simpl_symbols = find_symbols(ctx, simplified);
+                let symbols: Vec<_> = key_symbols.union(&simpl_symbols).cloned().collect();
+                solver.push()?;
+                for &sym in symbols.iter() {
+                    solver.declare_const(ctx, sym)?;
+                }
+                let not_eq = ctx.distinct(key, simplified);
+                solver.assert(ctx, not_eq)?;
+                match solver.check_sat()? {
+                    CheckSatResponse::Sat => {
+                        let key_value = solver.get_value(ctx, key)?;
+                        let simplified_value = solver.get_value(ctx, simplified)?;
+                        println!(
+                            "{} ({}) =/= ({}) {}",
+                            key.serialize_to_str(ctx),
+                            key_value.serialize_to_str(ctx),
+                            simplified_value.serialize_to_str(ctx),
+                            simplified.serialize_to_str(ctx)
+                        );
+                        let mut syms = vec![];
+                        for &sym in symbols.iter() {
+                            let value = solver.get_value(ctx, sym)?;
+                            syms.push(format!(
+                                "{}={}",
+                                sym.serialize_to_str(ctx),
+                                value.serialize_to_str(ctx)
+                            ));
+                        }
+                        println!(" w/ {}", syms.join(", "));
+                        incorrect += 1;
+                    }
+                    CheckSatResponse::Unsat => {
+                        correct += 1;
+                    } // OK
+                    CheckSatResponse::Unknown => {} // OK
+                }
+
+                solver.pop()?;
+            }
+        }
+        if incorrect > 0 {
+            println!(
+                "{incorrect} / {} simplifications were incorrect. See log.",
+                incorrect + correct
+            );
+        }
+
+        Ok(incorrect)
+    }
 }
 
 /// Simplifies one expression (not its children)
@@ -256,8 +319,11 @@ fn simplify_bv_and(ctx: &mut Context, a: ExprRef, b: ExprRef) -> Option<ExprRef>
                 // a & !a -> 0
                 (Expr::BVNot(inner, w), _) if *inner == b => Some(ctx.zero(*w)),
                 (_, Expr::BVNot(inner, w)) if *inner == a => Some(ctx.zero(*w)),
-                // !a & !b -> a | b
-                (Expr::BVNot(a, _), Expr::BVNot(b, _)) => Some(ctx.or(*a, *b)),
+                // !a & !b -> !(a | b)
+                (Expr::BVNot(a, _), Expr::BVNot(b, _)) => {
+                    let or = ctx.or(*a, *b);
+                    Some(ctx.not(or))
+                }
                 _ => None,
             }
         }
@@ -292,8 +358,11 @@ fn simplify_bv_or(ctx: &mut Context, a: ExprRef, b: ExprRef) -> Option<ExprRef>
                 // a | !a -> 1
                 (Expr::BVNot(inner, w), _) if *inner == b => Some(ctx.ones(*w)),
                 (_, Expr::BVNot(inner, w)) if *inner == a => Some(ctx.ones(*w)),
-                // !a | !b -> a & b
-                (Expr::BVNot(a, _), Expr::BVNot(b, _)) => Some(ctx.and(*a, *b)),
+                // !a | !b -> !(a & b)
+                (Expr::BVNot(a, _), Expr::BVNot(b, _)) => {
+                    let and = ctx.and(*a, *b);
+                    Some(ctx.not(and))
+                }
                 _ => None,
             }
         }