feat: handle exit points with unknown satisfiability

disable optimistic search space pruning, when generating
SMT-lib files.
fix a bug, which crashes the engine, when satisfiability is unknown.

benches/engine.rs

@@ -130,6 +130,7 @@ fn execute_symbolically<S: Solver, P: AsRef<Path>>(object_path: P) {
     let options = SymbolicExecutionOptions {
         max_exection_depth: 5000000,
         memory_size: ByteSize(400000),
+        ..Default::default()
     };
     let solver = S::default();
     let strategy = ShortestPathStrategy::compute_for(&program).unwrap();

src/engine/bug.rs

@@ -14,8 +14,7 @@ pub enum Bug<Info: BugInfo> {
 
     AccessToUnitializedMemory {
         info: Info,
-        instruction: Instruction,
-        operands: Vec<Info::Value>,
+        reason: UninitializedMemoryAccessReason<Info>,
     },
 
     AccessToUnalignedAddress {
@@ -29,6 +28,8 @@ pub enum Bug<Info: BugInfo> {
 
     ExitCodeGreaterZero {
         info: Info,
+        exit_code: u64,
+        address: u64,
     },
 }
 
@@ -39,16 +40,10 @@ where
     fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
         match self {
             Bug::DivisionByZero { info } => write!(f, "reason: division by zero\n{}", info),
-            Bug::AccessToUnitializedMemory {
-                info,
-                instruction,
-                operands,
-            } => write!(
+            Bug::AccessToUnitializedMemory { info, reason } => write!(
                 f,
-                "reason: access to uninitialized memory\ninstruction: {}\noperands {:?}\n{}",
-                instruction_to_str(*instruction),
-                operands,
-                info,
+                "reason: access to uninitialized memory\n{}\n{}",
+                info, reason,
             ),
             Bug::AccessToUnalignedAddress { info, address } => write!(
                 f,
@@ -60,7 +55,50 @@ where
                 "reason: accessed a memory address out of virtual address space\n{}",
                 info,
             ),
-            Bug::ExitCodeGreaterZero { info } => write!(f, "exit code greater than zero\n{}", info),
+            Bug::ExitCodeGreaterZero {
+                info,
+                exit_code,
+                address,
+            } => write!(
+                f,
+                "reason: exit code ({}) greater than zero at pc={:#x}\n{}",
+                exit_code, address, info
+            ),
+        }
+    }
+}
+
+#[derive(Debug, Clone)]
+pub enum UninitializedMemoryAccessReason<Info: BugInfo> {
+    ReadUnintializedMemoryAddress {
+        description: String,
+        address: u64,
+    },
+    InstructionWithUninitializedOperand {
+        instruction: Instruction,
+        operands: Vec<Info::Value>,
+    },
+}
+
+impl<Info> fmt::Display for UninitializedMemoryAccessReason<Info>
+where
+    Info: BugInfo,
+{
+    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
+        match self {
+            UninitializedMemoryAccessReason::InstructionWithUninitializedOperand {
+                instruction,
+                operands,
+            } => write!(
+                f,
+                "instruction: {}  operands: {:?}",
+                instruction_to_str(*instruction),
+                operands
+            ),
+            UninitializedMemoryAccessReason::ReadUnintializedMemoryAddress {
+                description,
+                address,
+            } => write!(f, "{} (pc: {:#x})", description, address),
         }
     }
 }

src/engine/rarity_simulation.rs

@@ -26,6 +26,8 @@
 //! The amount of iterations/cycles and the amount of states allows for a fine-grained control for
 //! finding bugs in depth or in breadth, respectively.
 
+use crate::engine::UninitializedMemoryAccessReason;
+
 use super::{
     system::{instruction_to_str, SyscallId},
     Bug as GenericBug, BugFinder, BugInfo, VirtualMemory,
@@ -461,7 +463,7 @@ impl Executor {
 
     fn execute(&mut self, instruction: Instruction) -> Result<Option<Bug>, RaritySimulationError> {
         match instruction {
-            Instruction::Ecall(_) => self.execute_ecall(instruction),
+            Instruction::Ecall(_) => self.execute_ecall(),
             Instruction::Lui(utype) => self.execute_lui(utype),
             Instruction::Addi(itype) => self.execute_itype(instruction, itype, u64::wrapping_add),
             Instruction::Add(rtype) => self.execute_rtype(instruction, rtype, u64::wrapping_add),
@@ -502,9 +504,11 @@ impl Executor {
                 inputs: self.concrete_inputs.clone(),
                 pc: self.state.pc,
             },
-            instruction,
-            // TODO: fix operands
-            operands: vec![],
+            reason: UninitializedMemoryAccessReason::InstructionWithUninitializedOperand {
+                instruction,
+                // TODO: fix operands
+                operands: vec![],
+            },
         }
     }
 
@@ -806,10 +810,7 @@ impl Executor {
         Ok(None)
     }
 
-    fn execute_write(
-        &mut self,
-        instruction: Instruction,
-    ) -> Result<Option<Bug>, RaritySimulationError> {
+    fn execute_write(&mut self) -> Result<Option<Bug>, RaritySimulationError> {
         if !matches!(self.state.regs[Register::A0 as usize], Value::Concrete(1)) {
             return not_supported("can not handle other fd than stdout in write syscall");
         }
@@ -852,8 +853,13 @@ impl Executor {
                         inputs: self.concrete_inputs.clone(),
                         pc: self.state.pc,
                     },
-                    instruction,
-                    operands: vec![],
+                    reason: UninitializedMemoryAccessReason::ReadUnintializedMemoryAddress {
+                        description: format!(
+                            "access to uninitialized memory in write syscall ({:#x})",
+                            self.state.pc
+                        ),
+                        address: self.state.pc,
+                    },
                 }));
             }
         }
@@ -915,6 +921,8 @@ impl Executor {
                             inputs: self.concrete_inputs.clone(),
                             pc: self.state.pc,
                         },
+                        exit_code,
+                        address: self.state.pc,
                     }))
                 } else {
                     trace!("exiting context with exit_code 0");
@@ -926,10 +934,7 @@ impl Executor {
         }
     }
 
-    fn execute_ecall(
-        &mut self,
-        instruction: Instruction,
-    ) -> Result<Option<Bug>, RaritySimulationError> {
+    fn execute_ecall(&mut self) -> Result<Option<Bug>, RaritySimulationError> {
         trace!("[{:#010x}] ecall", self.state.pc);
 
         let result = match self.state.regs[Register::A7 as usize] {
@@ -940,7 +945,7 @@ impl Executor {
                 self.execute_read()
             }
             Value::Concrete(syscall_id) if syscall_id == (SyscallId::Write as u64) => {
-                self.execute_write(instruction)
+                self.execute_write()
             }
             Value::Concrete(syscall_id) if syscall_id == (SyscallId::Exit as u64) => {
                 self.execute_exit()