wip: generate random inputs

Cargo.toml

@@ -8,3 +8,4 @@ patronus = "0.18.2"
 clap = { version = "4.5.14", features = ["derive"] }
 smallvec = { version = "1.13.2", features = ["union"] }
 petgraph = { version = "0.6.5" , features = []}
+rand = "0.8.5"

src/constraints.rs

@@ -36,6 +36,15 @@ impl ConstraintCluster {
         self.inputs.sort_unstable();
         self.inputs.dedup();
     }
+    pub fn exprs(&self) -> &ExprRefVec {
+        &self.exprs
+    }
+    pub fn states(&self) -> &ExprRefVec {
+        &self.states
+    }
+    pub fn inputs(&self) -> &ExprRefVec {
+        &self.inputs
+    }
 }
 
 /// Check to see which constraints we can fulfill
@@ -46,11 +55,11 @@ pub fn analyze_constraints(
 ) -> Vec<ConstraintCluster> {
     use petgraph::visit::NodeIndexable;
     let graph = extract_constraint_graph(ctx, sys, init);
-    println!("{:?}", petgraph::dot::Dot::new(&graph));
+    //println!("{:?}", petgraph::dot::Dot::new(&graph));
 
     // extract connected components from graph
     let groups = connected_components(&graph);
-    println!("{:?}", groups);
+    //println!("{:?}", groups);
 
     // turn components into constraint clusters
     let state_map = sys.state_map();

src/random.rs

@@ -4,10 +4,11 @@
 //
 // Random testing strategy to finding counter examples.
 
-use crate::constraints::analyze_constraints;
+use crate::constraints::{analyze_constraints, ConstraintCluster};
 use patronus::ir::*;
 use patronus::mc::Simulator;
 use patronus::sim::interpreter::{InitKind, Interpreter};
+use std::collections::HashSet;
 
 #[derive(Debug, Copy, Clone)]
 pub struct RandomOptions {
@@ -27,22 +28,86 @@ pub fn random_testing(
     sys: TransitionSystem,
     opts: RandomOptions,
 ) -> RandomResult {
+    // collect constraints for input randomization
+    let constraints = analyze_constraints(ctx, &sys, false);
+
+    // find out which inputs are unconstrained
+    let constrained_inputs = constraints
+        .iter()
+        .map(|c| c.inputs().to_vec())
+        .flatten()
+        .collect::<HashSet<_>>();
+    let unconstrained_inputs = sys
+        .get_signals(|s| s.is_input())
+        .iter()
+        .map(|(s, _)| *s)
+        .filter(|s| !constrained_inputs.contains(s))
+        .collect::<Vec<_>>();
+
+    // create simulator
     let sim_ctx = ctx.clone();
     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 system
-    println!("{}", sys.serialize_to_str(ctx));
-    let constraints = analyze_constraints(ctx, &sys, true);
-    println!("{:?}", constraints);
-
-    // TODO
+    // randomize our first inputs
+    randomize_inputs(ctx, &constraints, &unconstrained_inputs, &sys, &mut sim);
 
     RandomResult::None
 }
 
+fn randomize_inputs(
+    ctx: &Context,
+    constraints: &[ConstraintCluster],
+    unconstrained_inputs: &[ExprRef],
+    sys: &TransitionSystem,
+    sim: &mut Interpreter,
+) {
+    // randomize constrained inputs
+    for cluster in constraints.iter() {
+        loop {
+            // randomize all inputs in cluster
+            for input in cluster.inputs().iter() {
+                randomize_symbol(ctx, *input, sim);
+            }
+
+            // check to see if constraints are fulfilled
+            let ok = cluster
+                .exprs()
+                .iter()
+                .all(|expr| sim.get(*expr).unwrap().to_u64().unwrap() == 1);
+            // if they are, we are done here
+            if ok {
+                break;
+            }
+        }
+    }
+
+    // randomize other inputs
+    for input in unconstrained_inputs.iter() {
+        randomize_symbol(ctx, *input, sim);
+    }
+}
+
+fn randomize_symbol(ctx: &Context, symbol: ExprRef, sim: &mut Interpreter) {
+    match ctx.get(symbol).get_bv_type(ctx) {
+        Some(1) => {
+            todo!("generate 1-bit values");
+        }
+        Some(width) => {
+            if width <= 64 {
+                todo!("generate 64-bit values");
+            } else {
+                todo!("generate value wider than 64-bit");
+            }
+        }
+        None => {
+            todo!("support array type inputs");
+        }
+    }
+}
+
 #[cfg(test)]
 mod tests {
     use super::*;