feat: Limit read syscall

src/cli.rs

@@ -259,6 +259,13 @@ pub fn args() -> Command {
                         .allow_hyphen_values(true)
                         .num_args(1..)
                 )
+                .arg(
+                    Arg::new("benchmark")
+                        .help("Symbolicaly benchmark the model")
+                        .long("benchmark")
+                        .num_args(1)
+                        .value_parser(value_parser!(u64))
+                )
         )
         .subcommand(
             Command::new("qubot")

src/main.rs

@@ -19,9 +19,13 @@ use crate::unicorn::memory::replace_memory;
 use crate::unicorn::optimize::{optimize_model_with_input, optimize_model_with_solver};
 use crate::unicorn::qubot::{InputEvaluator, Qubot};
 use crate::unicorn::sat_solver::solve_bad_states;
+#[cfg(feature = "boolector")]
+use crate::unicorn::smt_solver::boolector_impl::*;
 use crate::unicorn::smt_solver::*;
 use crate::unicorn::unroller::{prune_model, renumber_model, unroll_model};
-use crate::unicorn::write_model;
+use crate::unicorn::{write_model, Model};
+#[cfg(feature = "boolector")]
+use boolector_solver::{SolverResult, BV};
 
 use ::unicorn::disassemble::disassemble;
 use ::unicorn::emulate::EmulatorState;
@@ -93,6 +97,7 @@ fn main() -> Result<()> {
             let emulate_model = is_beator && args.get_flag("emulate");
             let arg0 = expect_arg::<String>(args, "input-file")?;
             let extras = collect_arg_values(args, "extras");
+            let benchmark_max_input = args.get_one::<u64>("benchmark").cloned();
 
             let mut model = if !input_is_dimacs {
                 let mut model = if !input_is_btor2 {
@@ -158,6 +163,11 @@ fn main() -> Result<()> {
                 None
             };
 
+            // Test input limitation
+            if let (Some(max_input), Some(model)) = (benchmark_max_input, &model) {
+                run_symbolic_benchmark(model, max_input)?;
+            }
+
             if compile_model {
                 assert!(!input_is_btor2, "cannot compile arbitrary BTOR2");
                 assert!(!input_is_dimacs, "cannot compile arbitrary DIMACS");
@@ -294,6 +304,53 @@ fn main() -> Result<()> {
     }
 }
 
+fn run_symbolic_benchmark(model: &Model, max_input_size: u64) -> Result<()> {
+    #[cfg(feature = "boolector")]
+    let mut smt_solver: BoolectorSolver = BoolectorSolver::new(None);
+
+    for n in 0..=max_input_size {
+        println!("Finding bounds for input size: {n}");
+
+        // Create new constraint environment
+        smt_solver.solver.push(1);
+
+        // Assume input size is <= n
+        let max_input_bv = BV::from_u64(smt_solver.solver.clone(), n, 64);
+        let counter_bv = smt_solver.translate(&model.read_counter).into_bv();
+
+        println!(
+            "Comparing {} <= {}",
+            counter_bv.as_binary_str().unwrap_or("NONE".to_string()),
+            max_input_bv.as_binary_str().unwrap_or("NONE".to_string())
+        );
+
+        counter_bv.ulte(&max_input_bv).assert();
+
+        let result = smt_solver.solver.sat();
+        match result {
+            SolverResult::Sat => {
+                println!("SAT")
+            }
+            SolverResult::Unsat => {
+                println!("UNSAT")
+            }
+            SolverResult::Unknown => {
+                println!("UNKNOWN")
+            }
+        }
+
+        // TODO Find upper bound
+
+        // TODO Find lower bound
+
+        // TODO Add bound to the graph
+
+        smt_solver.solver.pop(1);
+    }
+
+    Ok(())
+}
+
 fn init_logger(cli_log_level: LogLevel) -> Result<()> {
     let log_level_env_var = "MONSTER_LOG";
     let log_style_env_var = "MONSTER_LOG_STYLE";

src/unicorn/btor2file_parser.rs

@@ -1,8 +1,10 @@
+use std::cell::RefCell;
 use std::collections::HashMap;
 use std::fs::File;
 use std::io::{self, BufRead};
 use std::ops::Range;
 use std::path::Path;
+use std::rc::Rc;
 
 #[cfg(feature = "gui")]
 use crate::guinea::MemoryData;
@@ -29,6 +31,7 @@ pub fn parse_btor2_file(path: &Path) -> Model {
         heap_range: Range { start: 0, end: 0 },
         stack_range: Range { start: 0, end: 0 },
         memory_size: 0,
+        read_counter: Rc::new(RefCell::new(Node::Comment("dummy".to_string()))),
     }
 }
 
@@ -62,6 +65,7 @@ pub fn parse_btor2_string(string: &str, data: &MemoryData) -> Model {
         heap_range: heap_start..heap_end,
         stack_range: stack_start..stack_end,
         memory_size: ByteSize::mib(data.memory_size).as_u64(),
+        read_counter: Rc::new(RefCell::new(Node::Comment("dummy".to_string()))),
     }
 }
 
@@ -414,6 +418,7 @@ mod tests_btor2_parser {
             heap_range: Range { start: 0, end: 0 },
             stack_range: Range { start: 0, end: 0 },
             memory_size: 0,
+            read_counter: Rc::new(RefCell::new(Node::Comment("dummy".to_string()))),
         }
     }
     #[test]

src/unicorn/builder.rs

@@ -70,6 +70,7 @@ struct ModelBuilder {
     stack_range: Range<u64>,
     current_nid: Nid,
     pc: u64,
+    read_counter: NodeRef,
 }
 
 struct InEdge {
@@ -111,7 +112,7 @@ impl ModelBuilder {
             division_flow: dummy_node.clone(),
             remainder_flow: dummy_node.clone(),
             access_flow: dummy_node.clone(),
-            ecall_flow: dummy_node,
+            ecall_flow: dummy_node.clone(),
             memory_size,
             max_heap_size: max_heap as u64 * size_of::<u64>() as u64,
             max_stack_size: max_stack as u64 * size_of::<u64>() as u64,
@@ -120,6 +121,7 @@ impl ModelBuilder {
             stack_range: 0..0,
             current_nid: 0,
             pc: 0,
+            read_counter: dummy_node,
         }
     }
 
@@ -133,6 +135,7 @@ impl ModelBuilder {
             heap_range: self.heap_range,
             stack_range: self.stack_range,
             memory_size: self.memory_size,
+            read_counter: self.read_counter,
         }
     }
 
@@ -1184,6 +1187,25 @@ impl ModelBuilder {
         self.new_ite(activate, self.one_bit.clone(), flow, NodeType::Bit)
     }
 
+    // Generate global read counter which tracks how many bytes were read
+    fn generate_read_counter(&mut self, should_read_occur: NodeRef, how_much_to_read: NodeRef) {
+        let constant = self.new_const(1000000);
+        let read_counter =
+            self.new_state(Some(constant), "read-counter".to_string(), NodeType::Word);
+
+        let possible_counter_value = self.new_add(how_much_to_read, read_counter.clone());
+        let next_counter_value = self.new_ite(
+            should_read_occur,
+            possible_counter_value,
+            read_counter.clone(),
+            NodeType::Word,
+        );
+
+        self.new_next(read_counter.clone(), next_counter_value, NodeType::Word);
+
+        self.read_counter = read_counter;
+    }
+
     fn generate_model(&mut self, program: &Program, argv: &[String]) -> Result<()> {
         let data_section_start = program.data.address;
         let data_section_end = program.data.address + program.data.content.len() as u64;
@@ -1350,17 +1372,23 @@ impl ModelBuilder {
             })
             .context("Failed to decode instructions of program")?;
 
+        // System calls
         self.new_comment("syscalls".to_string());
         self.current_nid = 40000000;
         let mut kernel_flow = self.kernel_mode.clone();
+
         let num_openat = self.new_const(SyscallId::Openat as u64);
         let is_openat = self.new_eq(self.reg_node(Register::A7), num_openat);
+
         let num_read = self.new_const(SyscallId::Read as u64);
         let is_read = self.new_eq(self.reg_node(Register::A7), num_read);
+
         let num_write = self.new_const(SyscallId::Write as u64);
         let is_write = self.new_eq(self.reg_node(Register::A7), num_write);
+
         let num_exit = self.new_const(SyscallId::Exit as u64);
         let is_exit = self.new_eq(self.reg_node(Register::A7), num_exit);
+
         let num_brk = self.new_const(SyscallId::Brk as u64);
         let is_brk = self.new_eq(self.reg_node(Register::A7), num_brk);
 
@@ -1373,6 +1401,7 @@ impl ModelBuilder {
             NodeType::Bit,
         );
 
+        // Read syscall
         self.current_nid = 42000000;
         let active_read = self.new_and_bit(self.ecall_flow.clone(), is_read.clone());
         kernel_flow = self.new_ite(
@@ -1391,50 +1420,58 @@ impl ModelBuilder {
         let read_const_8 = self.new_const(8);
         let read_full_word = self.new_ugte(read_remaining.clone(), read_const_8.clone());
         let read_bytes = self.new_ite(read_full_word, read_const_8, read_remaining, NodeType::Word);
+
         let read_input1 = self.new_input("1-byte-input".to_string(), NodeType::Input1Byte);
         let read_input2 = self.new_input("2-byte-input".to_string(), NodeType::Input2Byte);
-        let read_const_2 = self.new_const(2);
-        let read_bytes_eq_2 = self.new_eq(read_bytes.clone(), read_const_2);
-        let read_ite_2 = self.new_ite(read_bytes_eq_2, read_input2, read_input1, NodeType::Word);
         let read_input3 = self.new_input("3-byte-input".to_string(), NodeType::Input3Byte);
-        let read_const_3 = self.new_const(3);
-        let read_bytes_eq_3 = self.new_eq(read_bytes.clone(), read_const_3);
-        let read_ite_3 = self.new_ite(read_bytes_eq_3, read_input3, read_ite_2, NodeType::Word);
         let read_input4 = self.new_input("4-byte-input".to_string(), NodeType::Input4Byte);
-        let read_const_4 = self.new_const(4);
-        let read_bytes_eq_4 = self.new_eq(read_bytes.clone(), read_const_4);
-        let read_ite_4 = self.new_ite(read_bytes_eq_4, read_input4, read_ite_3, NodeType::Word);
         let read_input5 = self.new_input("5-byte-input".to_string(), NodeType::Input5Byte);
-        let read_const_5 = self.new_const(5);
-        let read_bytes_eq_5 = self.new_eq(read_bytes.clone(), read_const_5);
-        let read_ite_5 = self.new_ite(read_bytes_eq_5, read_input5, read_ite_4, NodeType::Word);
         let read_input6 = self.new_input("6-byte-input".to_string(), NodeType::Input6Byte);
-        let read_const_6 = self.new_const(6);
-        let read_bytes_eq_6 = self.new_eq(read_bytes.clone(), read_const_6);
-        let read_ite_6 = self.new_ite(read_bytes_eq_6, read_input6, read_ite_5, NodeType::Word);
         let read_input7 = self.new_input("7-byte-input".to_string(), NodeType::Input7Byte);
-        let read_const_7 = self.new_const(7);
-        let read_bytes_eq_7 = self.new_eq(read_bytes.clone(), read_const_7);
-        let read_ite_7 = self.new_ite(read_bytes_eq_7, read_input7, read_ite_6, NodeType::Word);
         let read_input8 = self.new_input("8-byte-input".to_string(), NodeType::Word);
+
+        let read_const_2 = self.new_const(2);
+        let read_const_3 = self.new_const(3);
+        let read_const_4 = self.new_const(4);
+        let read_const_5 = self.new_const(5);
+        let read_const_6 = self.new_const(6);
+        let read_const_7 = self.new_const(7);
         let read_const_8 = self.new_const(8);
+
+        let read_bytes_eq_2 = self.new_eq(read_bytes.clone(), read_const_2);
+        let read_bytes_eq_3 = self.new_eq(read_bytes.clone(), read_const_3);
+        let read_bytes_eq_4 = self.new_eq(read_bytes.clone(), read_const_4);
+        let read_bytes_eq_5 = self.new_eq(read_bytes.clone(), read_const_5);
+        let read_bytes_eq_6 = self.new_eq(read_bytes.clone(), read_const_6);
+        let read_bytes_eq_7 = self.new_eq(read_bytes.clone(), read_const_7);
         let read_bytes_eq_8 = self.new_eq(read_bytes.clone(), read_const_8);
+
+        let read_ite_2 = self.new_ite(read_bytes_eq_2, read_input2, read_input1, NodeType::Word);
+        let read_ite_3 = self.new_ite(read_bytes_eq_3, read_input3, read_ite_2, NodeType::Word);
+        let read_ite_4 = self.new_ite(read_bytes_eq_4, read_input4, read_ite_3, NodeType::Word);
+        let read_ite_5 = self.new_ite(read_bytes_eq_5, read_input5, read_ite_4, NodeType::Word);
+        let read_ite_6 = self.new_ite(read_bytes_eq_6, read_input6, read_ite_5, NodeType::Word);
+        let read_ite_7 = self.new_ite(read_bytes_eq_7, read_input7, read_ite_6, NodeType::Word);
         let read_ite_8 = self.new_ite(read_bytes_eq_8, read_input8, read_ite_7, NodeType::Word);
+
         let read_address = self.new_add(self.reg_node(Register::A1), self.reg_node(Register::A0));
         let read_store = self.new_write(read_address, read_ite_8);
+
         let read_more = self.new_ult(self.reg_node(Register::A0), self.reg_node(Register::A2));
         let read_more = self.new_and_bit(is_read.clone(), read_more);
         let read_not_done = self.new_and_bit(self.kernel_mode.clone(), read_more);
         let read_not_zero = self.new_ugt(read_bytes.clone(), self.zero_word.clone());
         let read_do_store = self.new_and_bit(read_not_done.clone(), read_not_zero);
+
         let read_ite_mem = self.new_ite(
-            read_do_store,
+            read_do_store.clone(),
             read_store,
             self.memory_flow.clone(),
             NodeType::Memory,
         );
         self.memory_flow = read_ite_mem;
-        let read_new_a0 = self.new_add(self.reg_node(Register::A0), read_bytes);
+
+        let read_new_a0 = self.new_add(self.reg_node(Register::A0), read_bytes.clone());
         let read_ite_a0 = self.new_ite(
             read_not_done.clone(),
             read_new_a0,
@@ -1449,6 +1486,8 @@ impl ModelBuilder {
             NodeType::Bit,
         );
 
+        self.generate_read_counter(read_do_store, read_bytes);
+
         self.current_nid = 45000000;
         let active_brk = self.new_and_bit(self.ecall_flow.clone(), is_brk.clone());
         let brk_init = self.new_const(self.heap_range.start);

src/unicorn/mod.rs

@@ -197,6 +197,7 @@ pub struct Model {
     pub heap_range: Range<u64>,
     pub stack_range: Range<u64>,
     pub memory_size: u64,
+    pub read_counter: NodeRef,
 }
 
 #[derive(Clone, Debug)]

src/unicorn/optimize.rs

@@ -737,18 +737,18 @@ impl<'a, S: SMTSolver> ConstantFolder<'a, S> {
                 match self.smt_solver.solve(cond) {
                     SMTSolution::Sat => {
                         warn!(
-                            "Bad state '{}' is satisfiable!",
+                            "3Bad state '{}' is satisfiable!",
                             name.as_deref().unwrap_or("?")
                         );
                         if terminate_on_bad {
                             // TODO: Change this to use return Result<> instead of panic!
-                            panic!("Bad state satisfiable");
+                            panic!("4Bad state satisfiable");
                         }
                         return true;
                     }
                     SMTSolution::Unsat => {
                         debug!(
-                            "Bad state '{}' is unsatisfiable, removing",
+                            "5Bad state '{}' is unsatisfiable, removing",
                             name.as_deref().unwrap_or("?")
                         );
                         return false;

src/unicorn/sat_solver.rs

@@ -72,7 +72,7 @@ fn process_single_bad_state<S: SATSolver>(
             match solution {
                 SATSolution::Sat => {
                     warn!(
-                        "Bad state '{}' is satisfiable ({})!",
+                        "1Bad state '{}' is satisfiable ({})!",
                         name.as_deref().unwrap_or("?"),
                         S::name()
                     );
@@ -82,7 +82,7 @@ fn process_single_bad_state<S: SATSolver>(
                 }
                 SATSolution::Unsat => {
                     debug!(
-                        "Bad state '{}' is unsatisfiable ({}).",
+                        "2Bad state '{}' is unsatisfiable ({}).",
                         name.as_deref().unwrap_or("?"),
                         S::name()
                     );