From 4da06238c5b4ea999f02c8bca3925e09922da48b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Kevin=20L=C3=A4ufer?= <laeufer@cs.berkeley.edu>
Date: Thu, 18 Apr 2024 10:32:59 -0400
Subject: [PATCH] implement unrolling study

---
 synth/src/main.rs              |  3 +-
 synth/src/studies/unrolling.rs | 81 ++++++++++++++++++++++++++++++----
 2 files changed, 74 insertions(+), 10 deletions(-)

diff --git a/synth/src/main.rs b/synth/src/main.rs
index cb48eba..439f2a6 100644
--- a/synth/src/main.rs
+++ b/synth/src/main.rs
@@ -310,7 +310,8 @@ fn main() {
             rep.run().expect("failed to execute windowing exploration")
         }
         RepairCommand::UnrollingStudy => {
-            unrolling(repair_ctx).expect("failed to run unrolling study")
+            unrolling(repair_ctx, &args.solver.cmd(), args.smt_dump.as_deref())
+                .expect("failed to run unrolling study")
         }
     };
 
diff --git a/synth/src/studies/unrolling.rs b/synth/src/studies/unrolling.rs
index 00e8200..2ad6b48 100644
--- a/synth/src/studies/unrolling.rs
+++ b/synth/src/studies/unrolling.rs
@@ -6,15 +6,78 @@
 
 use crate::basic::generate_minimal_repair;
 use crate::repair::{RepairContext, RepairResult, RepairStatus};
-use crate::Stats;
-use libpatron::mc::{Simulator, TransitionSystemEncoding};
+use crate::start_solver;
+use crate::testbench::{RunConfig, StepInt, StopAt};
+use libpatron::mc::{Simulator, SmtSolverCmd, UnrollSmtEncoding};
+use serde::Serialize;
+use std::time::Instant;
 
-pub fn unrolling<S: Simulator, E: TransitionSystemEncoding>(
-    mut rctx: RepairContext<S, E>,
-) -> crate::repair::Result<RepairResult> {
-    let res = generate_minimal_repair(&mut rctx, 0, None)?;
-    let stats = Stats::default();
-    match res {
+#[derive(Debug, Serialize)]
+struct Stats {
+    /// the maximum number of steps we looked at
+    tb_len: StepInt,
+    /// how many steps we unrolled for
+    end_step: StepInt,
+    /// whether a correct repair was found
+    success: bool,
+    /// for incorrect repairs, where did the test fail
+    first_fail_at: Option<StepInt>,
+    /// execution time in ns
+    time_ns: u128,
+    /// minimum number of changes, None if no repair found
+    min_repair_size: Option<u64>,
+}
+
+pub fn unrolling<S>(
+    mut rctx: RepairContext<S, UnrollSmtEncoding>,
+    cmd: &SmtSolverCmd,
+    dump_smt: Option<&str>,
+) -> crate::repair::Result<RepairResult>
+where
+    S: Simulator,
+    S::SnapshotId: Clone,
+{
+    // remember the starting state
+    let start_state = rctx.sim.take_snapshot();
+    let mut res = None;
+    let tb_len = rctx.tb.step_count();
+    for end_step in 0..tb_len {
+        // start new smt solver to isolate performance
+        (rctx.smt_ctx, rctx.enc) = start_solver(cmd, dump_smt, rctx.ctx, rctx.sys)?;
+        let start = Instant::now();
+        res = generate_minimal_repair(&mut rctx, 0, Some(end_step))?;
+        let time_ns = start.elapsed().as_nanos();
+
+        // check to see if we got a good repair
+        let mut min_repair_size = None;
+        let mut first_fail_at = None;
+        if let Some((repair, min_num_changes)) = &res {
+            min_repair_size = Some(*min_num_changes as u64);
+
+            // try out repair to see if we were actually successful
+            rctx.sim.restore_snapshot(start_state.clone());
+            rctx.synth_vars.apply_to_sim(&mut rctx.sim, repair);
+            let conf = RunConfig {
+                start: 0,
+                stop: StopAt::first_fail(),
+            };
+            first_fail_at = rctx.tb.run(&mut rctx.sim, &conf, false).first_fail_at;
+        }
+
+        let success = res.is_some() && first_fail_at.is_none();
+        let s = Stats {
+            tb_len,
+            end_step,
+            success,
+            time_ns,
+            min_repair_size,
+            first_fail_at,
+        };
+        println!("{}", serde_json::to_string(&s).unwrap());
+    }
+
+    let stats = crate::Stats::default();
+    match &res {
         None => Ok(RepairResult {
             status: RepairStatus::CannotRepair,
             stats,
@@ -23,7 +86,7 @@ pub fn unrolling<S: Simulator, E: TransitionSystemEncoding>(
         Some((repair, _)) => Ok(RepairResult {
             status: RepairStatus::Success,
             stats,
-            solutions: vec![repair],
+            solutions: vec![repair.clone()],
         }),
     }
 }