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/smtlib2.rs b/src/backends/smtlib2.rs index f953326..968b160 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; @@ -260,12 +261,35 @@ 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); + + } return (Ok(result), SMTRes::Sat(res.clone(), Some(read_result))); }, _ => {} } - (Ok(result), check_sat.clone()) } } 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)); } }