From 5bc4598f0903daa68c677b0bf2657a888447b25d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Kevin=20L=C3=A4ufer?= Date: Fri, 8 Dec 2023 21:34:22 -0500 Subject: [PATCH] getting a solution with the simple synthesizer --- synth/.gitignore | 4 +++ synth/Cargo.lock | 4 +-- synth/Cargo.toml | 3 +++ synth/basic.smt | 41 ----------------------------- synth/src/basic.rs | 63 ++++++++++++++++++++++++++++++++++++++++++--- synth/src/main.rs | 12 ++++++--- synth/src/repair.rs | 2 +- 7 files changed, 79 insertions(+), 50 deletions(-) create mode 100644 synth/.gitignore delete mode 100644 synth/basic.smt diff --git a/synth/.gitignore b/synth/.gitignore new file mode 100644 index 0000000..d386a7c --- /dev/null +++ b/synth/.gitignore @@ -0,0 +1,4 @@ +basic.smt +flamegraph.svg +perf.data +perf.data.old diff --git a/synth/Cargo.lock b/synth/Cargo.lock index 54324d2..876381c 100644 --- a/synth/Cargo.lock +++ b/synth/Cargo.lock @@ -216,9 +216,9 @@ checksum = "89d92a4743f9a61002fae18374ed11e7973f530cb3a3255fb354818118b2203c" [[package]] name = "libpatron" -version = "0.6.0" +version = "0.6.3" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "48b5282658c89ed4c355df8b7691d6d4e7f3213a9bfabbfbba7fb2278038a7e9" +checksum = "07130132b0b00d2f05a6161fa68427e4f5f68a61cd45f983ea8a17c9645c7fe8" dependencies = [ "codespan-reporting", "easy-smt", diff --git a/synth/Cargo.toml b/synth/Cargo.toml index 57885ee..a05e254 100644 --- a/synth/Cargo.toml +++ b/synth/Cargo.toml @@ -13,3 +13,6 @@ memmap2 = "0.9.0" num-bigint = "0.4.4" num-traits = "0.2.17" serde_json = { version = "1.0.108", features = ["preserve_order"] } + +[profile.release] +debug = 1 \ No newline at end of file diff --git a/synth/basic.smt b/synth/basic.smt deleted file mode 100644 index 1323d0d..0000000 --- a/synth/basic.smt +++ /dev/null @@ -1,41 +0,0 @@ -(set-option :print-success true) -(set-option :produce-models true) -(set-logic QF_ABV) -(declare-const __synth_literal_8@0 (_ BitVec 8)) -(declare-const __synth_change_literal_8@0 Bool) -(declare-const __synth_literal_9@0 (_ BitVec 8)) -(declare-const __synth_change_literal_9@0 Bool) -(declare-const __synth_literal_7@0 (_ BitVec 4)) -(declare-const __synth_change_literal_7@0 Bool) -(declare-const __synth_literal_10@0 (_ BitVec 8)) -(declare-const __synth_change_literal_10@0 Bool) -(declare-const __synth_literal_6@0 (_ BitVec 4)) -(declare-const __synth_change_literal_6@0 Bool) -(declare-const __synth_literal_11@0 (_ BitVec 8)) -(declare-const __synth_change_literal_11@0 Bool) -(declare-const __synth_literal_5@0 (_ BitVec 4)) -(declare-const __synth_change_literal_5@0 Bool) -(declare-const __synth_literal_12@0 (_ BitVec 8)) -(declare-const __synth_change_literal_12@0 Bool) -(declare-const __synth_literal_4@0 (_ BitVec 4)) -(declare-const __synth_change_literal_4@0 Bool) -(declare-const __synth_literal_13@0 (_ BitVec 8)) -(declare-const __synth_change_literal_13@0 Bool) -(declare-const __synth_literal_3@0 (_ BitVec 4)) -(declare-const __synth_change_literal_3@0 Bool) -(declare-const __synth_literal_14@0 (_ BitVec 8)) -(declare-const __synth_change_literal_14@0 Bool) -(declare-const __synth_literal_2@0 (_ BitVec 4)) -(declare-const __synth_change_literal_2@0 Bool) -(declare-const __synth_literal_15@0 (_ BitVec 8)) -(declare-const __synth_change_literal_15@0 Bool) -(declare-const __synth_literal_1@0 (_ BitVec 4)) -(declare-const __synth_change_literal_1@0 Bool) -(declare-const __synth_literal_16@0 (_ BitVec 8)) -(declare-const __synth_change_literal_16@0 Bool) -(declare-const __synth_literal_0@0 (_ BitVec 4)) -(declare-const __synth_change_literal_0@0 Bool) -(declare-const en@0 Bool) -(declare-const C@0 Bool) -(declare-const B@0 Bool) -(declare-const A@0 Bool) diff --git a/synth/src/basic.rs b/synth/src/basic.rs index 2f2bc04..1796b61 100644 --- a/synth/src/basic.rs +++ b/synth/src/basic.rs @@ -2,10 +2,11 @@ // released under BSD 3-Clause License // author: Kevin Laeufer -use crate::repair::{RepairAssignment, RepairVars}; +use crate::repair::{RepairAssignment, RepairVars, CHANGE_COUNT_WIDTH}; use crate::testbench::Testbench; use crate::Solver; use easy_smt as smt; +use easy_smt::Response; use libpatron::ir::*; use libpatron::mc::{Simulator, SmtSolverCmd, TransitionSystemEncoding, UnrollSmtEncoding}; use libpatron::sim::interpreter::ValueRef; @@ -25,6 +26,7 @@ pub fn basic_repair( sim: &impl Simulator, tb: &Testbench, conf: &BasicConfig, + change_count_ref: ExprRef, ) -> Result>> { let mut smt_ctx = create_smt_ctx(&conf.solver, conf.dump_file.as_deref())?; @@ -36,17 +38,72 @@ pub fn basic_repair( // constrain starting state to that from the simulator constrain_starting_state(sys, synth_vars, sim, &enc, &mut smt_ctx)?; + let start_unroll = std::time::Instant::now(); // unroll system and constrain inputs and outputs for _ in 0..(tb.step_count() - 1) { enc.unroll(&mut smt_ctx)?; } + if conf.verbose { + println!( + "Took {:?} to unroll", + std::time::Instant::now() - start_unroll + ); + } + + let start_apply_const = std::time::Instant::now(); tb.apply_constraints(&mut smt_ctx, &enc)?; + if conf.verbose { + println!( + "Took {:?} to apply constraints", + std::time::Instant::now() - start_apply_const + ); + } // check to see if a solution exists + let start_check = std::time::Instant::now(); let r = smt_ctx.check()?; - println!("{r:?}"); + let check_duration = std::time::Instant::now() - start_check; + if conf.verbose { + println!("Check-Sat took {check_duration:?}"); + } + match r { + // cannot find a repair + Response::Unsat | Response::Unknown => return Ok(None), + Response::Sat => {} // OK, continue + } + + // find a minimal repair + let min_num_changes = minimize_changes(&mut smt_ctx, change_count_ref, &enc)?; + if conf.verbose { + println!("Found a minimal solution with {min_num_changes} changes.") + } + + let solution = synth_vars.read_assignment(&mut smt_ctx, &enc); + Ok(Some(vec![solution])) +} - Ok(None) +fn minimize_changes( + smt_ctx: &mut smt::Context, + change_count_ref: ExprRef, + enc: &impl TransitionSystemEncoding, +) -> Result { + let mut num_changes = 1u32; + let change_count_expr = enc.get_at(smt_ctx, change_count_ref, 0); + loop { + let constraint = smt_ctx.eq( + change_count_expr, + smt_ctx.binary(CHANGE_COUNT_WIDTH as usize, num_changes), + ); + match smt_ctx.check_assuming([constraint])? { + Response::Sat => { + // found a solution + return Ok(num_changes); + } + Response::Unsat => {} + Response::Unknown => panic!("SMT solver returned unknown!"), + } + num_changes += 1; + } } fn constrain_starting_state( diff --git a/synth/src/main.rs b/synth/src/main.rs index b6fb10d..16bf6a7 100644 --- a/synth/src/main.rs +++ b/synth/src/main.rs @@ -103,7 +103,7 @@ fn main() { } // add a change count to the system - add_change_count(&mut ctx, &mut sys, &synth_vars.change); + let change_count_ref = add_change_count(&mut ctx, &mut sys, &synth_vars.change); // print system if args.verbose { @@ -158,6 +158,7 @@ fn main() { sim.restore_snapshot(start_state); // call to the synthesizer + let start_synth = std::time::Instant::now(); let repair = if args.incremental { todo!("implement incremental synthesizer") } else { @@ -166,9 +167,13 @@ fn main() { verbose: args.verbose, dump_file: Some("basic.smt".to_string()), }; - basic_repair(&ctx, &sys, &synth_vars, &sim, &tb, &conf) + basic_repair(&ctx, &sys, &synth_vars, &sim, &tb, &conf, change_count_ref) .expect("failed to execute basic synthesizer") }; + let synth_duration = std::time::Instant::now() - start_synth; + if args.verbose { + println!("Synthesizer took {synth_duration:?}"); + } // print status let (status, solutions) = match repair { @@ -176,7 +181,8 @@ fn main() { Some(assignments) => { let mut res = Vec::with_capacity(assignments.len()); for aa in assignments.iter() { - res.push(synth_vars.to_json(&ctx, aa)); + let assignment_json = synth_vars.to_json(&ctx, aa); + res.push(json!({"assignment": assignment_json})); } ("success", json!(res)) } diff --git a/synth/src/repair.rs b/synth/src/repair.rs index 8043b0f..ff6f51d 100644 --- a/synth/src/repair.rs +++ b/synth/src/repair.rs @@ -112,7 +112,7 @@ pub struct RepairAssignment { } const CHANGE_COUNT_OUTPUT_NAME: &str = "__change_count"; -const CHANGE_COUNT_WIDTH: WidthInt = 16; +pub const CHANGE_COUNT_WIDTH: WidthInt = 16; pub fn add_change_count( ctx: &mut Context,