From b05c5748a944fdc156f9e46af7902755c1531258 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Kevin=20L=C3=A4ufer?= <laeufer@cornell.edu>
Date: Wed, 28 Aug 2024 22:14:33 -0400
Subject: [PATCH] fix missing constraints

---
 .github/workflows/test.yml |  4 ++--
 Cargo.toml                 |  2 +-
 src/constraints.rs         |  4 ++--
 src/main.rs                | 11 ++++++++++-
 src/random.rs              | 27 +++++++++++++++++++++++++++
 5 files changed, 42 insertions(+), 6 deletions(-)

diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml
index 47a59a7..76a2910 100644
--- a/.github/workflows/test.yml
+++ b/.github/workflows/test.yml
@@ -45,6 +45,6 @@ jobs:
           submodules: 'true'
       - name: Build
         run: cargo build --verbose
-      - name: Run on Shift Register w/ Depth 16
-        run: cargo run -- hwmcc19/hwmcc19-single-benchmarks/btor2/bv/mann/data-integrity/unsafe/shift_register_top_w64_d16_e0.btor2
+      - name: Run on Shift Register w/ Depth 16 for 100k cycles
+        run: cargo run -- --max-cycles=100000 hwmcc19/hwmcc19-single-benchmarks/btor2/bv/mann/data-integrity/unsafe/shift_register_top_w64_d16_e0.btor2
 
diff --git a/Cargo.toml b/Cargo.toml
index ff87a0f..a39aff1 100644
--- a/Cargo.toml
+++ b/Cargo.toml
@@ -4,7 +4,7 @@ version = "0.1.0"
 edition = "2021"
 
 [dependencies]
-patronus = {  version = "0.18.3" }
+patronus = {  version = "0.18.5" }
 clap = { version = "4.5.14", features = ["derive"] }
 smallvec = { version = "1.13.2", features = ["union"] }
 petgraph = { version = "0.6.5" , features = []}
diff --git a/src/constraints.rs b/src/constraints.rs
index cd79849..a84a769 100644
--- a/src/constraints.rs
+++ b/src/constraints.rs
@@ -55,11 +55,9 @@ pub fn analyze_constraints(
 ) -> Vec<ConstraintCluster> {
     use petgraph::visit::NodeIndexable;
     let graph = extract_constraint_graph(ctx, sys, init);
-    //println!("{:?}", petgraph::dot::Dot::new(&graph));
 
     // extract connected components from graph
     let groups = connected_components(&graph);
-    //println!("{:?}", groups);
 
     // turn components into constraint clusters
     let state_map = sys.state_map();
@@ -133,6 +131,8 @@ fn extract_constraint_graph(
                     // constraint creates a connection
                     out.add_edge(var_to_node[&leaf], var_to_node[other], expr_ref);
                 }
+                // we always need a self edge (in case there is only one leaf)
+                out.add_edge(var_to_node[&leaf], var_to_node[&leaf], expr_ref);
             }
         }
     }
diff --git a/src/main.rs b/src/main.rs
index 0876118..1b4de71 100644
--- a/src/main.rs
+++ b/src/main.rs
@@ -21,6 +21,8 @@ use std::fmt::{Debug, Formatter};
 struct Args {
     #[arg(short, long)]
     verbose: bool,
+    #[arg(long)]
+    max_cycles: Option<u64>,
     #[arg(value_name = "BTOR2", index = 1)]
     filename: String,
 }
@@ -29,6 +31,7 @@ static RANDOM_OPTS: RandomOptions = RandomOptions {
     small_k: 50,
     large_k: 1_000,
     large_k_prob: 0.01,
+    max_cycles: None,
 };
 
 fn main() {
@@ -45,7 +48,9 @@ fn main() {
     simplify_expressions(&mut ctx, &mut sys);
 
     // try random testing
-    match random_testing(ctx, sys, RANDOM_OPTS) {
+    let mut options = RANDOM_OPTS.clone();
+    options.max_cycles = args.max_cycles;
+    match random_testing(ctx, sys, options) {
         ModelCheckResult::Unknown => {
             // print nothing
         }
@@ -110,6 +115,10 @@ impl Witness {
         if sys.states().count() > 0 {
             writeln!(out, "#0")?;
             for (ii, (_, state)) in sys.states().enumerate() {
+                if state.init.is_some() {
+                    // the state has a computed init value
+                    continue;
+                }
                 let name = state
                     .symbol
                     .get_symbol_name(ctx)
diff --git a/src/random.rs b/src/random.rs
index a1a3bf5..615e8f4 100644
--- a/src/random.rs
+++ b/src/random.rs
@@ -12,6 +12,7 @@ use patronus::mc::Simulator;
 use patronus::sim::interpreter::{InitKind, Interpreter};
 use rand::{Rng, SeedableRng};
 use std::collections::HashSet;
+use std::num::NonZeroU64;
 
 #[derive(Debug, Copy, Clone)]
 pub struct RandomOptions {
@@ -21,6 +22,8 @@ pub struct RandomOptions {
     pub large_k: u64,
     /// probability of sampling a large instead of a small k
     pub large_k_prob: f64,
+    /// maximum number of cycles to execute
+    pub max_cycles: Option<u64>,
 }
 
 pub fn random_testing(
@@ -28,6 +31,8 @@ pub fn random_testing(
     sys: TransitionSystem,
     opts: RandomOptions,
 ) -> ModelCheckResult {
+    // println!("{}", sys.serialize_to_str(&ctx));
+
     // collect constraints for input randomization
     let constraints = analyze_constraints(&mut ctx, &sys, false);
 
@@ -65,6 +70,7 @@ pub fn random_testing(
     let mut rng = rand_xoshiro::Xoshiro256PlusPlus::seed_from_u64(1);
 
     // main loop
+    let mut cycle_count = 0;
     loop {
         let k_max = sample_k_max(&mut rng, &opts);
 
@@ -105,6 +111,13 @@ pub fn random_testing(
 
             // advance the system
             sim.step();
+            cycle_count += 1;
+            if let Some(max_cycles) = opts.max_cycles {
+                if max_cycles <= cycle_count {
+                    println!("Exciting after executing {} cycles.", cycle_count);
+                    return ModelCheckResult::Unknown;
+                }
+            }
         }
     }
     ModelCheckResult::Unknown
@@ -153,6 +166,20 @@ fn record_witness(
 
         // TODO: remove
         sim.update();
+
+        // sanity check constraints
+        for cluster in constraints.iter() {
+            for expr in cluster.exprs() {
+                let is_ok = sim.get(*expr).unwrap().to_u64().unwrap() == 1;
+                debug_assert!(
+                    is_ok,
+                    "{k}: failed {} in {:?}",
+                    ctx.get(*expr).serialize_to_str(ctx),
+                    cluster
+                );
+            }
+        }
+
         if k == k_bad {
             // sanity check bad
             let bads = check_for_bad_states(ctx, bad_states, sim);