From 77c8ae3f26f67e199d8048c3f1c8ba4296b16a9e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Kevin=20L=C3=A4ufer?= <laeufer@cs.berkeley.edu>
Date: Mon, 19 Aug 2024 14:15:13 -0400
Subject: [PATCH] add split conjunction heper function

---
 Cargo.toml    |   1 +
 src/random.rs | 110 +++++++++++++++++++++++++++++++++++++++++++-------
 2 files changed, 96 insertions(+), 15 deletions(-)

diff --git a/Cargo.toml b/Cargo.toml
index 31f516c..489278f 100644
--- a/Cargo.toml
+++ b/Cargo.toml
@@ -6,3 +6,4 @@ edition = "2021"
 [dependencies]
 patronus = "0.18.0"
 clap = { version = "4.5.14", features = ["derive"] }
+smallvec = { version = "1.13.2", features = ["union"] }
diff --git a/src/random.rs b/src/random.rs
index af305ff..9e058b9 100644
--- a/src/random.rs
+++ b/src/random.rs
@@ -4,11 +4,10 @@
 //
 // Random testing strategy to finding counter examples.
 
-use patronus::ir::{
-    cone_of_influence, cone_of_influence_comb, cone_of_influence_init, Context, ExprRef, GetNode,
-    SerializableIrNode, TransitionSystem, TypeCheck,
-};
-use patronus::sim;
+use patronus::ir::*;
+use patronus::mc::Simulator;
+use patronus::sim::interpreter::{InitKind, Interpreter};
+use smallvec::{smallvec, SmallVec};
 
 #[derive(Debug, Copy, Clone)]
 pub struct RandomOptions {
@@ -29,7 +28,10 @@ pub fn random_testing(
     opts: RandomOptions,
 ) -> RandomResult {
     let sim_ctx = ctx.clone();
-    let mut sim = sim::interpreter::Interpreter::new(&sim_ctx, &sys);
+    let mut sim = Interpreter::new(&sim_ctx, &sys);
+
+    // we initialize all states to zero, since most bugs are not reset initialization bugs
+    sim.init(InitKind::Zero);
 
     // // show all inputs
     // let inputs = sys.get_signals(|s| s.is_input());
@@ -58,6 +60,8 @@ pub fn random_testing(
     RandomResult::None
 }
 
+/// randomize all inputs
+
 struct Constraints {
     /// Single input constraints can be checked when we are sampling the input.
     /// The tuple is (constraint ref, input ref)
@@ -68,16 +72,23 @@ struct Constraints {
     others: Vec<ExprRef>,
 }
 
+type ExprRefVec = SmallVec<[ExprRef; 4]>;
+
+/// A number of constraints that connect several inputs/states together.
 #[derive(Debug, Clone)]
-struct Constraint {
-    expr: ExprRef,
-    inputs: Vec<ExprRef>,
-    states: Vec<ExprRef>,
+struct ConstraintCluster {
+    exprs: ExprRefVec,
+    inputs: ExprRefVec,
+    states: ExprRefVec,
 }
 
 /// Check to see which constraints we can fulfill
-fn analyze_constraints(ctx: &Context, sys: &TransitionSystem, init: bool) -> Vec<Constraint> {
-    let states = sys.state_map();
+fn analyze_constraints(
+    ctx: &Context,
+    sys: &TransitionSystem,
+    init: bool,
+) -> Vec<ConstraintCluster> {
+    let state_map = sys.state_map();
     let mut out = Vec::new();
     // we want to see which constraints depends on which inputs
     for (expr_ref, info) in sys.constraints() {
@@ -87,9 +98,9 @@ fn analyze_constraints(ctx: &Context, sys: &TransitionSystem, init: bool) -> Vec
         } else {
             cone_of_influence_comb(ctx, sys, expr_ref)
         };
-        let (states, inputs) = cone.iter().partition(|e| states.contains_key(e));
-        let constraint = Constraint {
-            expr: expr_ref,
+        let (states, inputs) = cone.into_iter().partition(|e| state_map.contains_key(e));
+        let constraint = ConstraintCluster {
+            exprs: smallvec![expr_ref],
             inputs,
             states,
         };
@@ -97,3 +108,72 @@ fn analyze_constraints(ctx: &Context, sys: &TransitionSystem, init: bool) -> Vec
     }
     out
 }
+
+fn split_conjunction(ctx: &mut Context, e: ExprRef) -> ExprRefVec {
+    let mut out = smallvec![];
+    let mut todo: ExprRefVec = smallvec![e];
+    while let Some(e) = todo.pop() {
+        match ctx.get(e) {
+            Expr::BVAnd(a, b, 1) => {
+                todo.push(*b);
+                todo.push(*a);
+            }
+            Expr::BVNot(e2, 1) => match *ctx.get(*e2) {
+                Expr::BVOr(a, b, 1) => {
+                    todo.push(ctx.not(b));
+                    todo.push(ctx.not(a));
+                }
+                _ => out.push(e),
+            },
+            _ => out.push(e),
+        }
+    }
+    out
+}
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+
+    #[test]
+    fn type_size() {
+        // one ExprRef is 1/2 a pointer, thus 4 ExprRef fit into two pointer sized memory slots
+        assert_eq!(std::mem::size_of::<ExprRef>(), 4);
+        // we scale the ExprRefVec to be the same size on stack as a Vec<ExprRef>
+        assert_eq!(
+            std::mem::size_of::<ExprRefVec>(),
+            std::mem::size_of::<Vec<ExprRef>>()
+        );
+    }
+
+    #[test]
+    fn test_split_conjunction() {
+        let mut ctx = Context::default();
+        let a = ctx.bv_symbol("a", 1);
+        let b = ctx.bv_symbol("b", 1);
+        let c = ctx.bv_symbol("b", 1);
+        assert_eq!(split_conjunction(&mut ctx, a), [a].into());
+        let a_and_b = ctx.and(a, b);
+        assert_eq!(split_conjunction(&mut ctx, a_and_b), [a, b].into());
+        let a_and_b_and_c_1 = ctx.and(a_and_b, c);
+        assert_eq!(
+            split_conjunction(&mut ctx, a_and_b_and_c_1),
+            [a, b, c].into()
+        );
+        let b_and_c = ctx.and(b, c);
+        let a_and_b_and_c_2 = ctx.and(a, b_and_c);
+        assert_eq!(
+            split_conjunction(&mut ctx, a_and_b_and_c_2),
+            [a, b, c].into()
+        );
+        let a_or_b = ctx.or(a, b);
+        assert_eq!(split_conjunction(&mut ctx, a_or_b), [a_or_b].into());
+        let not_a_or_b = ctx.not(a_or_b);
+        let not_a = ctx.not(a);
+        let not_b = ctx.not(b);
+        assert_eq!(
+            split_conjunction(&mut ctx, not_a_or_b),
+            [not_a, not_b].into()
+        );
+    }
+}