re-enable extraction of results in SMTBackend.solve, fix examples

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 {

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 {

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.");

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");
     }
 
 }
-

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<L: Logic> SMTBackend for SMTLib2<L> {
         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<var>[0-9a-zA-Z_]+) \(\) [(]?[ _a-zA-Z0-9]+[)]?\n\s+(?P<val>([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::<u64>()
+                              }
+                              .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())
     }
 }

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));
     }
 }