From f466772792cd9d0edededc0b0f1bd02bf9746e42 Mon Sep 17 00:00:00 2001 From: Bobby Powers Date: Tue, 1 Nov 2016 14:27:59 -0400 Subject: [PATCH 1/4] Revert "bug fix for hanging. works on osx & ubuntu" This reverts commit b672e5e326c2908bdeaa2d109d2493500e2316e9. --- src/backends/smtlib2.rs | 29 ++++++++++++++++++++++++++++- 1 file changed, 28 insertions(+), 1 deletion(-) diff --git a/src/backends/smtlib2.rs b/src/backends/smtlib2.rs index f953326..09c08bd 100644 --- a/src/backends/smtlib2.rs +++ b/src/backends/smtlib2.rs @@ -260,12 +260,39 @@ impl SMTBackend for SMTLib2 { match check_sat { SMTRes::Sat(ref res, _) => { smt_proc.write("(get-model)\n".to_owned()); + // XXX: For some reason we need two reads here in order to get the result from + // the SMT solver. Need to look into the reason for this. This might stop + // working in the + // future. + //let _ = smt_proc.read(); let read_result = smt_proc.read_getmodel_output(); + let re = Regex::new(r"\s+\(define-fun (?P[0-9a-zA-Z_]+) \(\) [(]?[ _a-zA-Z0-9]+[)]?\n\s+(?P([0-9]+|#x[0-9a-f]+|#b[01]+))") + .unwrap(); + + /* + for caps in re.captures_iter(&read_result) { + // Here the caps.name("val") can be a hex value, or a binary value or a decimal + // value. We need to parse the output to a u64 accordingly. + let val_str = caps.name("val").unwrap(); + let val = if val_str.len() > 2 && &val_str[0..2] == "#x" { + u64::from_str_radix(&val_str[2..], 16) + } else if val_str.len() > 2 && &val_str[0..2] == "#b" { + u64::from_str_radix(&val_str[2..], 2) + } else { + val_str.parse::() + } + .unwrap(); + let vname = caps.name("var").unwrap(); + result.insert(self.var_map[vname].0.clone(), val); + + } + */ + smt_proc.write("(exit)\n".to_owned()); return (Ok(result), SMTRes::Sat(res.clone(), Some(read_result))); }, _ => {} } - + smt_proc.write("(exit)\n".to_owned()); (Ok(result), check_sat.clone()) } } From b7e7adb1afa841b5b419dff3c2152d0815265632 Mon Sep 17 00:00:00 2001 From: Bobby Powers Date: Tue, 1 Nov 2016 14:32:29 -0400 Subject: [PATCH 2/4] backends/smtlib2: re-enable extracting result in solve() --- src/backends/smtlib2.rs | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/backends/smtlib2.rs b/src/backends/smtlib2.rs index 09c08bd..b665df4 100644 --- a/src/backends/smtlib2.rs +++ b/src/backends/smtlib2.rs @@ -6,6 +6,7 @@ use std::process::{Child}; use std::collections::{HashMap}; use std::io::{Read, Write}; +use regex::Regex; use petgraph::graph::{Graph, NodeIndex}; use petgraph::EdgeDirection; @@ -269,7 +270,6 @@ impl SMTBackend for SMTLib2 { let re = Regex::new(r"\s+\(define-fun (?P[0-9a-zA-Z_]+) \(\) [(]?[ _a-zA-Z0-9]+[)]?\n\s+(?P([0-9]+|#x[0-9a-f]+|#b[01]+))") .unwrap(); - /* for caps in re.captures_iter(&read_result) { // Here the caps.name("val") can be a hex value, or a binary value or a decimal // value. We need to parse the output to a u64 accordingly. @@ -286,7 +286,6 @@ impl SMTBackend for SMTLib2 { result.insert(self.var_map[vname].0.clone(), val); } - */ smt_proc.write("(exit)\n".to_owned()); return (Ok(result), SMTRes::Sat(res.clone(), Some(read_result))); }, From 5b0c04b06e2f88de227363a540110bdf0680bda9 Mon Sep 17 00:00:00 2001 From: Bobby Powers Date: Tue, 1 Nov 2016 14:36:15 -0400 Subject: [PATCH 3/4] API + crate name updates for examples + tests --- examples/bajr.rs | 20 ++++++++++---------- examples/bitvec_x86_64.rs | 18 +++++++++--------- examples/fiestel.rs | 16 ++++++++-------- examples/simple_example.rs | 21 ++++++++++----------- src/backends/z3.rs | 9 ++++++--- 5 files changed, 43 insertions(+), 41 deletions(-) diff --git a/examples/bajr.rs b/examples/bajr.rs index f15286a..7aa782d 100644 --- a/examples/bajr.rs +++ b/examples/bajr.rs @@ -15,21 +15,21 @@ // (assert (> x 1)) // (assert (> y 1)) -// The libsmt library is designed to simplify this process of interacting with Z3 and enable to do so programmatically through Rust +// The rustproof_libsmt library is designed to simplify this process of interacting with Z3 and enable to do so programmatically through Rust -// Import the libsmt library -extern crate libsmt; +// Import the rustproof_libsmt library +extern crate rustproof_libsmt; -use libsmt::backends::smtlib2::*; -use libsmt::backends::backend::*; -use libsmt::backends::z3; +use rustproof_libsmt::backends::smtlib2::*; +use rustproof_libsmt::backends::backend::*; +use rustproof_libsmt::backends::z3; // Include the Int theory and its functions -use libsmt::theories::{core,integer}; +use rustproof_libsmt::theories::{core,integer}; // Include the LIA logic -use libsmt::logics::lia::LIA; +use rustproof_libsmt::logics::lia::LIA; fn main() { @@ -51,7 +51,7 @@ fn main() { // Defining the assert conditions //let cond1 = solver.assert(integer::OpCodes::Add, &[x, y]); //let _ = solver.assert(integer::OpCodes::Gt, &[cond1, int5]); - //let _ = solver.assert(integer::OpCodes::Gt, &[x, int1]); + //let _ = solver.assert(integer::OpCodes::Gt, &[x, int1]); //let _ = solver.assert(integer::OpCodes::Gt, &[y, bool1]); //let _ = solver.assert(integer::OpCodes::Lt, &[x, int5]); let _ = solver.assert(core::OpCodes::And, &[bool1, bool1]); @@ -62,7 +62,7 @@ fn main() { // SMTRes::Error(..) => { println!("{}", z3.read()); }, // } - let (res, check) = solver.solve(&mut z3); + let (res, check) = solver.solve(&mut z3, false); match res { Ok(..) => { match check { diff --git a/examples/bitvec_x86_64.rs b/examples/bitvec_x86_64.rs index 376a7a0..2743a8b 100644 --- a/examples/bitvec_x86_64.rs +++ b/examples/bitvec_x86_64.rs @@ -16,14 +16,14 @@ // mov [rax], rsi // ret -extern crate libsmt; +extern crate rustproof_libsmt; -use libsmt::backends::smtlib2::*; -use libsmt::backends::backend::*; -use libsmt::backends::z3; -use libsmt::theories::{array_ex, bitvec, core}; -use libsmt::logics::qf_abv::QF_ABV; -use libsmt::logics::qf_abv; +use rustproof_libsmt::backends::smtlib2::*; +use rustproof_libsmt::backends::backend::*; +use rustproof_libsmt::backends::z3; +use rustproof_libsmt::theories::{array_ex, bitvec, core}; +use rustproof_libsmt::logics::qf_abv::QF_ABV; +use rustproof_libsmt::logics::qf_abv; macro_rules! bv_const { ($solver: ident, $i: expr, $n: expr) => { $solver.new_const(bitvec::OpCodes::Const($i, $n)) } @@ -62,7 +62,7 @@ fn main() { }; // Adding constraints based on the above asm. - + // Reset memory to 0 solver.assert(core::OpCodes::Cmp, &[mem, const_mem_0]); // We know that the return address is at rbp + 0x4 @@ -83,7 +83,7 @@ fn main() { solver.assert(core::OpCodes::Cmp, &[sel, const_badcafe]); // Check if we have a satisfying solution. - if let Ok(result) = solver.solve(&mut z3) { + if let (Ok(result), _) = solver.solve(&mut z3, false) { println!("Out-Of-Bounds Write detected!"); println!("rdi: 0x{:x}; rsi: 0x{:x};", result[&rdi], result[&rsi]); } else { diff --git a/examples/fiestel.rs b/examples/fiestel.rs index d8fb1f8..9da5fb7 100644 --- a/examples/fiestel.rs +++ b/examples/fiestel.rs @@ -3,14 +3,14 @@ // Though Z3 was unable to solve the 17 round fiestel network that was a part of the // challenge, this serves as a good example for the usage of this library. -#[macro_use] extern crate libsmt; +#[macro_use] extern crate rustproof_libsmt; -use libsmt::backends::smtlib2::*; -use libsmt::backends::backend::*; -use libsmt::backends::z3; -use libsmt::theories::{bitvec, core}; -use libsmt::logics::qf_abv::QF_ABV; -use libsmt::logics::qf_abv; +use rustproof_libsmt::backends::smtlib2::*; +use rustproof_libsmt::backends::backend::*; +use rustproof_libsmt::backends::z3; +use rustproof_libsmt::theories::{bitvec, core}; +use rustproof_libsmt::logics::qf_abv::QF_ABV; +use rustproof_libsmt::logics::qf_abv; fn main() { @@ -50,7 +50,7 @@ fn main() { let _ = solver.assert(core::OpCodes::Cmp, &[rt, rt_const]); // Print the required keys. - if let Ok(result) = solver.solve(&mut z3) { + if let (Ok(result), _) = solver.solve(&mut z3, false) { println!("LK: {:x}; RK: {:x}", result[&lk], result[&rk]); } else { println!("No Solution."); diff --git a/examples/simple_example.rs b/examples/simple_example.rs index 10dff3c..3a2fb23 100644 --- a/examples/simple_example.rs +++ b/examples/simple_example.rs @@ -15,21 +15,21 @@ // (assert (> x 1)) // (assert (> y 1)) -// The libsmt library is designed to simplify this process of interacting with Z3 and enable to do so programmatically through Rust +// The rustproof_libsmt library is designed to simplify this process of interacting with Z3 and enable to do so programmatically through Rust -// Import the libsmt library -extern crate libsmt; +// Import the rustproof_libsmt library +extern crate rustproof_libsmt; -use libsmt::backends::smtlib2::*; -use libsmt::backends::backend::*; -use libsmt::backends::z3; +use rustproof_libsmt::backends::smtlib2::*; +use rustproof_libsmt::backends::backend::*; +use rustproof_libsmt::backends::z3; // Include the Int theory and its functions -use libsmt::theories::{integer}; +use rustproof_libsmt::theories::{integer}; // Include the LIA logic -use libsmt::logics::lia::LIA; +use rustproof_libsmt::logics::lia::LIA; fn main() { @@ -49,14 +49,13 @@ fn main() { // Defining the assert conditions let cond1 = solver.assert(integer::OpCodes::Add, &[x, y]); let _ = solver.assert(integer::OpCodes::Gt, &[cond1, int5]); - let _ = solver.assert(integer::OpCodes::Gt, &[x, int1]); + let _ = solver.assert(integer::OpCodes::Gt, &[x, int1]); let _ = solver.assert(integer::OpCodes::Gt, &[y, int1]); - if let Ok(result) = solver.solve(&mut z3) { + if let (Ok(result), _) = solver.solve(&mut z3, false) { println!("x: {}; y: {}", result[&x], result[&y]); } else { println!("No solutions for x and y found for given set of constraints"); } } - diff --git a/src/backends/z3.rs b/src/backends/z3.rs index 0092d35..bb3b9f4 100644 --- a/src/backends/z3.rs +++ b/src/backends/z3.rs @@ -67,7 +67,8 @@ mod test { let c = solver.new_const(integer::OpCodes::Const(10)); solver.assert(core::OpCodes::Cmp, &[x, c]); solver.assert(integer::OpCodes::Gt, &[x, y]); - let result = solver.solve(&mut z3).unwrap(); + let (result, _) = solver.solve(&mut z3, false); + let result = result.unwrap(); assert_eq!(result[&x], 10); assert_eq!(result[&y], 9); } @@ -83,7 +84,8 @@ mod test { solver.assert(core::OpCodes::Cmp, &[x, c]); let x_xor_y = solver.assert(bitvec::OpCodes::BvXor, &[x, y]); solver.assert(core::OpCodes::Cmp, &[x_xor_y, c8]); - let result = solver.solve(&mut z3).unwrap(); + let (result, _) = solver.solve(&mut z3, false); + let result = result.unwrap(); assert_eq!(result[&x], 10); assert_eq!(result[&y], 2); } @@ -96,7 +98,8 @@ mod test { let c4 = solver.new_const(bitvec::OpCodes::Const(0b100, 4)); let x_31_28 = solver.assert(bitvec::OpCodes::Extract(31, 28), &[x]); solver.assert(core::OpCodes::Cmp, &[x_31_28, c4]); - let result = solver.solve(&mut z3).unwrap(); + let (result, _) = solver.solve(&mut z3, false); + let result = result.unwrap(); assert_eq!(result[&x], (0b100 << 28)); } } From af47a3ce5cbacc607d809a79c0ca504ce92ffb9f Mon Sep 17 00:00:00 2001 From: Bobby Powers Date: Tue, 1 Nov 2016 14:41:44 -0400 Subject: [PATCH 4/4] backends/smtlib2: don't tell solver to exit when calling solve() And definitely don't do it twice if we've got a Satisfiable result. We might want to iteratively invoke solve(). --- src/backends/smtlib2.rs | 2 -- 1 file changed, 2 deletions(-) diff --git a/src/backends/smtlib2.rs b/src/backends/smtlib2.rs index b665df4..968b160 100644 --- a/src/backends/smtlib2.rs +++ b/src/backends/smtlib2.rs @@ -286,12 +286,10 @@ impl SMTBackend for SMTLib2 { result.insert(self.var_map[vname].0.clone(), val); } - smt_proc.write("(exit)\n".to_owned()); return (Ok(result), SMTRes::Sat(res.clone(), Some(read_result))); }, _ => {} } - smt_proc.write("(exit)\n".to_owned()); (Ok(result), check_sat.clone()) } }