synth: wip incremental

synth/src/incremental.rs

@@ -2,7 +2,7 @@
 // released under BSD 3-Clause License
 // author: Kevin Laeufer <[email protected]>
 
-use crate::testbench::{StepInt, Testbench};
+use crate::testbench::{RunConfig, StepInt, StopAt, Testbench};
 use easy_smt as smt;
 use libpatron::ir::*;
 use libpatron::mc::*;
@@ -60,15 +60,30 @@ where
         let mut past_k = self.fail_at;
         let mut future_k = self.fail_at;
 
-        while past_k + future_k <= self.max_window {}
+        while past_k + future_k <= self.max_window {
+            assert!(past_k >= self.fail_at);
+            let start_step = self.fail_at - past_k;
+            let end_step = self.fail_at + future_k;
+
+            // check to see if we can reproduce the error with the simulator
+            self.update_sim_state_to_step(start_step);
+            let conf = RunConfig {
+                start: start_step,
+                stop: StopAt::first_fail_or_step(end_step),
+            };
+            let res = self.tb.run(self.sim, &conf, false);
+            assert_eq!(res.first_fail_at, Some(self.fail_at));
+
+            todo!("synthesize solutions")
+        }
 
         todo!("implement incremental repair")
     }
 
-    fn get_state_at(&mut self, step: StepInt) -> S::SnapshotId {
+    fn update_sim_state_to_step(&mut self, step: StepInt) {
         assert!(step < self.tb.step_count());
         if let Some(snapshot_id) = self.snapshots.get(&step) {
-            snapshot_id.clone()
+            self.sim.restore_snapshot(snapshot_id.clone());
         } else {
             // find nearest step, _before_ the step we are going for
             let mut nearest_step = 0;
@@ -81,12 +96,16 @@ where
             }
 
             // go from nearest snapshot to the point where we want to take a snapshot
-            todo!();
+            self.sim.restore_snapshot(nearest_id.unwrap());
+            let run_conf = RunConfig {
+                start: nearest_step,
+                stop: StopAt::step(step),
+            };
+            self.tb.run(self.sim, &run_conf, self.verbose);
 
-            // take new snapshot and remember
+            // remember the state in case we need to go back
             let new_snapshot = self.sim.take_snapshot();
             self.snapshots.insert(step, new_snapshot.clone());
-            new_snapshot
         }
     }
 }

synth/src/main.rs

@@ -140,7 +140,8 @@ fn main() {
     let res = tb.run(
         &mut sim,
         &RunConfig {
-            stop: StopAt::FirstFail,
+            start: 0,
+            stop: StopAt::first_fail(),
         },
         args.verbose,
     );

synth/src/testbench.rs

@@ -49,12 +49,40 @@ impl RunResult {
 }
 
 pub struct RunConfig {
+    pub start: StepInt,
     pub stop: StopAt,
 }
 
-pub enum StopAt {
-    FirstFail,
-    End,
+pub struct StopAt {
+    at_first_fail: bool,
+    at_step: Option<StepInt>,
+}
+
+impl StopAt {
+    pub fn end() -> Self {
+        Self {
+            at_first_fail: false,
+            at_step: None,
+        }
+    }
+    pub fn first_fail() -> Self {
+        Self {
+            at_first_fail: true,
+            at_step: None,
+        }
+    }
+    pub fn step(step: StepInt) -> Self {
+        Self {
+            at_first_fail: false,
+            at_step: Some(step),
+        }
+    }
+    pub fn first_fail_or_step(step: StepInt) -> Self {
+        Self {
+            at_first_fail: true,
+            at_step: Some(step),
+        }
+    }
 }
 
 impl Testbench {
@@ -126,8 +154,16 @@ impl Testbench {
 
     pub fn run(&self, sim: &mut impl Simulator, conf: &RunConfig, verbose: bool) -> RunResult {
         let mut failures = Vec::new();
+        let last_step_plus_one = match conf.stop.at_step {
+            Some(step) => {
+                assert!(step < self.step_count());
+                step + 1
+            }
+            None => self.step_count(),
+        };
+        assert!(conf.start < last_step_plus_one);
 
-        for step_id in 0..self.step_count() {
+        for step_id in conf.start..last_step_plus_one {
             let range = self.step_range(step_id);
             self.do_step(
                 step_id as StepInt,
@@ -137,15 +173,14 @@ impl Testbench {
                 verbose,
             );
             // early exit
-            if !failures.is_empty() && matches!(conf.stop, StopAt::FirstFail) {
+            if !failures.is_empty() && conf.stop.at_first_fail {
                 return RunResult {
                     first_fail_at: Some(step_id as StepInt),
                 };
             }
         }
-        // success
         RunResult {
-            first_fail_at: None,
+            first_fail_at: failures.first().map(|f| f.step),
         }
     }