use super::{
bug::{Bug as GenericBug, BugInfo},
symbolic_state::{Query, QueryResult, SymbolicState, SymbolicValue, Witness},
system::{instruction_to_str, SyscallId},
UninitializedMemoryAccessReason,
};
use crate::{
path_exploration::ExplorationStrategy,
solver::{BVOperator, Solver, SolverError},
BugFinder,
};
use byteorder::{ByteOrder, LittleEndian};
use bytesize::ByteSize;
use log::{debug, trace};
use riscu::{
decode, types::*, DecodingError, Instruction, Program, ProgramSegment, Register,
INSTRUCTION_SIZE as INSTR_SIZE,
};
use std::{fmt, mem::size_of, sync::Arc};
use thiserror::Error;
const INSTRUCTION_SIZE: u64 = INSTR_SIZE as u64;
pub mod defaults {
use super::*;
pub const MEMORY_SIZE: ByteSize = ByteSize(bytesize::MIB);
pub const MAX_EXECUTION_DEPTH: u64 = 1000;
pub const OPTIMISTICALLY_PRUNE_SEARCH_SPACE: bool = true;
}
pub type SymbolicExecutionBug = GenericBug<SymbolicExecutionBugInfo>;
pub type SymbolicExecutionResult = Result<Option<SymbolicExecutionBug>, SymbolicExecutionError>;
type Bug = SymbolicExecutionBug;
#[derive(Clone, Copy, Debug)]
pub struct SymbolicExecutionOptions {
pub memory_size: ByteSize,
pub max_exection_depth: u64,
pub optimistically_prune_search_space: bool,
}
impl Default for SymbolicExecutionOptions {
fn default() -> Self {
Self {
memory_size: defaults::MEMORY_SIZE,
max_exection_depth: defaults::MAX_EXECUTION_DEPTH,
optimistically_prune_search_space: defaults::OPTIMISTICALLY_PRUNE_SEARCH_SPACE,
}
}
}
pub struct SymbolicExecutionEngine<'a, E, S>
where
E: ExplorationStrategy,
S: Solver,
{
options: SymbolicExecutionOptions,
strategy: &'a E,
solver: &'a S,
}
impl<'a, E, S> SymbolicExecutionEngine<'a, E, S>
where
E: ExplorationStrategy,
S: Solver,
{
pub fn new(options: &SymbolicExecutionOptions, strategy: &'a E, solver: &'a S) -> Self {
Self {
options: *options,
strategy,
solver,
}
}
}
impl<'a, E, S> BugFinder<SymbolicExecutionBugInfo, SymbolicExecutionError>
for SymbolicExecutionEngine<'a, E, S>
where
E: ExplorationStrategy,
S: Solver,
{
fn search_for_bugs(
&self,
program: &Program,
) -> Result<Option<GenericBug<SymbolicExecutionBugInfo>>, SymbolicExecutionError> {
let mut executor =
SymbolicExecutor::new(program, &self.options, self.strategy, self.solver);
let result = executor.run();
match result.expect_err("every run has to stop with an error") {
SymbolicExecutionError::ExecutionDepthReached(_)
| SymbolicExecutionError::ProgramExit(_)
| SymbolicExecutionError::NotReachable => Ok(None),
SymbolicExecutionError::BugFound(bug) => Ok(Some(bug)),
err => Err(err),
}
}
}
#[derive(Clone, Copy, Debug, Eq, Hash, PartialEq)]
pub enum Value {
Concrete(u64),
Symbolic(SymbolicValue),
Uninitialized,
}
impl fmt::Display for Value {
fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
match self {
Value::Concrete(c) => write!(f, "{:#x}", c),
Value::Symbolic(i) => write!(f, "x{}", i.index()),
Value::Uninitialized => write!(f, "uninit"),
}
}
}
#[derive(Debug, Clone, Error)]
pub enum SymbolicExecutionError {
#[error("failed to load binary {0:#}")]
IoError(Arc<anyhow::Error>),
#[error("engine does not support {0}")]
NotSupported(String),
#[error("has reached the maximum execution depth of {0}")]
ExecutionDepthReached(u64),
#[error("failed to decode instruction at PC: {0:#010x}")]
InvalidInstructionEncoding(u64, DecodingError),
#[error("fatal error in SMT solver")]
Solver(SolverError),
#[error("found a bug")]
BugFound(Bug),
#[error("exit syscall called with code: {0}")]
ProgramExit(Value),
#[error("program state is not reachable")]
NotReachable,
}
pub struct SymbolicExecutor<'a, E, S>
where
E: ExplorationStrategy,
S: Solver,
{
symbolic_state: Box<SymbolicState<'a, S>>,
program_break: u64,
pc: u64,
regs: [Value; 32],
memory: Vec<Value>,
strategy: &'a E,
options: SymbolicExecutionOptions,
execution_depth: u64,
amount_of_file_descriptors: u64,
}
impl<'a, E, S> SymbolicExecutor<'a, E, S>
where
E: ExplorationStrategy,
S: Solver,
{
pub fn new(
program: &Program,
options: &SymbolicExecutionOptions,
strategy: &'a E,
solver: &'a S,
) -> Self {
let mut regs = [Value::Uninitialized; 32];
let memory_size = options.memory_size.as_u64();
let mut memory = vec![Value::Uninitialized; memory_size as usize / 8];
let sp = memory_size - 8;
regs[Register::Sp as usize] = Value::Concrete(sp);
regs[Register::Zero as usize] = Value::Concrete(0);
let argc = 0;
memory[sp as usize / size_of::<u64>()] = Value::Concrete(argc);
load_segment(&mut memory, &program.code);
load_segment(&mut memory, &program.data);
let pc = program.code.address;
let program_break = program.data.address + program.data.content.len() as u64;
let symbolic_state = Box::new(SymbolicState::new(solver));
debug!(
"initializing new execution context with {} of main memory",
memory_size
);
debug!(
"code segment: start={:#x} length={}",
program.code.address,
program.code.content.len(),
);
debug!(
"data segment: start={:#x} length={}",
program.data.address,
program.data.content.len(),
);
debug!(
"init state: pc={:#x} brk={:#x}, argc={}",
pc, program_break, argc
);
Self {
symbolic_state,
program_break,
pc,
regs,
memory,
strategy,
execution_depth: 0,
options: *options,
amount_of_file_descriptors: 3,
}
}
fn decode(&self, raw: u32) -> Result<Instruction, SymbolicExecutionError> {
decode(raw).map_err(|e| SymbolicExecutionError::InvalidInstructionEncoding(self.pc, e))
}
fn run(&mut self) -> Result<(), SymbolicExecutionError> {
loop {
if self.execution_depth >= self.options.max_exection_depth {
trace!("maximum execution depth reached => exiting this context");
return Err(SymbolicExecutionError::ExecutionDepthReached(
self.execution_depth,
));
}
self.execution_depth += 1;
self.fetch()
.and_then(|raw| self.decode(raw))
.and_then(|instr| self.execute(instr))?;
}
}
fn execute_query(&mut self, query: Query) -> Result<QueryResult, SymbolicExecutionError> {
self.symbolic_state
.execute_query(query)
.map_err(SymbolicExecutionError::Solver)
}
fn access_to_uninitialized_memory(
&mut self,
instruction: Instruction,
v1: Value,
v2: Value,
) -> Result<(), SymbolicExecutionError> {
trace!(
"{}: {}, {} => computing reachability",
instruction_to_str(instruction),
v1,
v2
);
let result = self.execute_query(Query::Reachable)?;
let info = match result {
QueryResult::Sat(witness) => self.collect_bug_info(Some(witness)),
_ => self.collect_bug_info(None),
};
trace!("access to uninitialized memory => exiting");
Err(SymbolicExecutionError::BugFound(
self.access_to_uninitialized_memory_bug(
info,
UninitializedMemoryAccessReason::InstructionWithUninitializedOperand {
instruction,
operands: vec![v1, v2],
},
),
))
}
fn collect_bug_info(&self, witness: Option<Witness>) -> SymbolicExecutionBugInfo {
SymbolicExecutionBugInfo {
witness,
pc: self.pc,
}
}
fn access_to_unaligned_address_bug(&self, info: SymbolicExecutionBugInfo) -> Bug {
Bug::AccessToUnalignedAddress {
info,
address: self.pc,
}
}
fn access_to_uninitialized_memory_bug(
&self,
info: SymbolicExecutionBugInfo,
reason: UninitializedMemoryAccessReason<SymbolicExecutionBugInfo>,
) -> Bug {
Bug::AccessToUnitializedMemory { info, reason }
}
fn access_to_out_of_range_address_bug(&self, info: SymbolicExecutionBugInfo) -> Bug {
Bug::AccessToOutOfRangeAddress { info }
}
fn divison_by_zero_bug(&self, info: SymbolicExecutionBugInfo) -> Bug {
Bug::DivisionByZero { info }
}
fn exit_code_greater_zero_bug(&self, info: SymbolicExecutionBugInfo, exit_code: Value) -> Bug {
Bug::ExitCodeGreaterZero {
info,
exit_code,
address: self.pc,
}
}
fn exit_anyway_with_bug<F>(
&self,
result: QueryResult,
info_to_bug: F,
) -> Result<(), SymbolicExecutionError>
where
F: FnOnce(SymbolicExecutionBugInfo) -> Bug,
{
let info = self.collect_bug_info(match result {
QueryResult::Sat(witness) => Some(witness),
QueryResult::UnSat | QueryResult::Unknown => None,
});
let bug = info_to_bug(info);
Err(SymbolicExecutionError::BugFound(bug))
}
fn exit_anyway_with_bug_if_sat<F>(
&self,
result: QueryResult,
info_to_bug: F,
err_if_unsat: SymbolicExecutionError,
) -> Result<(), SymbolicExecutionError>
where
F: FnOnce(SymbolicExecutionBugInfo) -> Bug,
{
match result {
QueryResult::Sat(witness) => {
let bug = info_to_bug(self.collect_bug_info(Some(witness)));
Err(SymbolicExecutionError::BugFound(bug))
}
QueryResult::UnSat | QueryResult::Unknown => Err(err_if_unsat),
}
}
fn exit_with_bug_if_sat<F>(
&self,
result: QueryResult,
info_to_bug: F,
) -> Result<(), SymbolicExecutionError>
where
F: FnOnce(SymbolicExecutionBugInfo) -> Bug,
{
match result {
QueryResult::Sat(witness) => {
let bug = info_to_bug(self.collect_bug_info(Some(witness)));
Err(SymbolicExecutionError::BugFound(bug))
}
QueryResult::UnSat | QueryResult::Unknown => Ok(()),
}
}
fn is_in_vaddr_range(&self, vaddr: u64) -> bool {
vaddr as usize / size_of::<u64>() < self.memory.len()
}
fn check_for_valid_memory_address(
&mut self,
instruction: &str,
address: u64,
) -> Result<(), SymbolicExecutionError> {
let is_alignment_ok = address % size_of::<u64>() as u64 == 0;
if !is_alignment_ok {
trace!(
"{}: address {:#x} is not double word aligned => computing reachability",
instruction,
address
);
self.execute_query(Query::Reachable).and_then(|r| {
self.exit_anyway_with_bug(r, |i| self.access_to_unaligned_address_bug(i))
})
} else if !self.is_in_vaddr_range(address) {
trace!(
"{}: address {:#x} out of virtual address range (0x0 - {:#x}) => computing reachability",
instruction,
address,
self.memory.len() * size_of::<u64>(),
);
self.execute_query(Query::Reachable).and_then(|r| {
self.exit_anyway_with_bug(r, |i| self.access_to_out_of_range_address_bug(i))
})
} else {
Ok(())
}
}
fn check_for_valid_memory_range(
&mut self,
instruction: &str,
address: u64,
size: u64,
) -> Result<(), SymbolicExecutionError> {
if !self.is_in_vaddr_range(address) || !self.is_in_vaddr_range(address + size) {
trace!(
"{}: buffer {:#x} - {:#x} out of virtual address range (0x0 - {:#x}) => computing reachability",
instruction,
address,
address + size,
self.memory.len() * size_of::<u64>(),
);
self.execute_query(Query::Reachable).and_then(|r| {
self.exit_anyway_with_bug(r, |i| self.access_to_out_of_range_address_bug(i))
})
} else {
Ok(())
}
}
#[allow(clippy::unnecessary_wraps)]
fn execute_lui(&mut self, utype: UType) -> Result<(), SymbolicExecutionError> {
let immediate = u64::from(utype.imm()) << 12;
let result = Value::Concrete(immediate);
trace!(
"[{:#010x}] {}: {:?} <- {}",
self.pc,
instruction_to_str(Instruction::Lui(utype)),
utype.rd(),
result,
);
self.assign_rd(utype.rd(), result);
self.pc += INSTRUCTION_SIZE;
Ok(())
}
fn execute_divu_remu<Op>(
&mut self,
instruction: Instruction,
rtype: RType,
op: Op,
) -> Result<(), SymbolicExecutionError>
where
Op: FnOnce(u64, u64) -> u64,
{
match self.regs[rtype.rs2() as usize] {
Value::Symbolic(divisor) => {
trace!(
"{}: symbolic divisor -> find input for divisor == 0",
instruction_to_str(instruction)
);
self.execute_query(Query::Equals((divisor, 0)))
.and_then(|r| self.exit_with_bug_if_sat(r, |i| self.divison_by_zero_bug(i)))?;
}
Value::Concrete(divisor) if divisor == 0 => {
trace!(
"{}: divisor == 0 -> compute reachability",
instruction_to_str(instruction)
);
return self
.execute_query(Query::Reachable)
.and_then(|r| self.exit_anyway_with_bug(r, |i| self.divison_by_zero_bug(i)));
}
_ => {}
};
self.execute_rtype(instruction, rtype, op)
}
fn execute_itype<Op>(
&mut self,
instruction: Instruction,
itype: IType,
op: Op,
) -> Result<(), SymbolicExecutionError>
where
Op: FnOnce(u64, u64) -> u64,
{
let rs1_value = self.regs[itype.rs1() as usize];
let imm_value = Value::Concrete(itype.imm() as u64);
self.execute_binary_op(instruction, rs1_value, imm_value, itype.rd(), op)
}
fn execute_rtype<Op>(
&mut self,
instruction: Instruction,
rtype: RType,
op: Op,
) -> Result<(), SymbolicExecutionError>
where
Op: FnOnce(u64, u64) -> u64,
{
let rs1_value = self.regs[rtype.rs1() as usize];
let rs2_value = self.regs[rtype.rs2() as usize];
self.execute_binary_op(instruction, rs1_value, rs2_value, rtype.rd(), op)
}
fn execute_binary_op<Op>(
&mut self,
instruction: Instruction,
lhs: Value,
rhs: Value,
rd: Register,
op: Op,
) -> Result<(), SymbolicExecutionError>
where
Op: FnOnce(u64, u64) -> u64,
{
let result = match (lhs, rhs) {
(Value::Concrete(v1), Value::Concrete(v2)) => Value::Concrete(op(v1, v2)),
(Value::Symbolic(v1), Value::Concrete(v2)) => {
let v2 = self.symbolic_state.create_const(v2);
Value::Symbolic(self.symbolic_state.create_instruction(instruction, v1, v2))
}
(Value::Concrete(v1), Value::Symbolic(v2)) => {
let v1 = self.symbolic_state.create_const(v1);
Value::Symbolic(self.symbolic_state.create_instruction(instruction, v1, v2))
}
(Value::Symbolic(v1), Value::Symbolic(v2)) => {
Value::Symbolic(self.symbolic_state.create_instruction(instruction, v1, v2))
}
_ => {
return self.access_to_uninitialized_memory(instruction, lhs, rhs);
}
};
trace!(
"[{:#010x}] {}: {}, {} |- {:?} <- {}",
self.pc,
instruction_to_str(instruction),
lhs,
rhs,
rd,
result,
);
self.assign_rd(rd, result);
self.pc += INSTRUCTION_SIZE;
Ok(())
}
fn execute_brk(&mut self) -> Result<(), SymbolicExecutionError> {
if let Value::Concrete(new_program_break) = self.regs[Register::A0 as usize] {
let old_program_break = self.program_break;
if new_program_break < self.program_break || !self.is_in_vaddr_range(new_program_break)
{
self.regs[Register::A0 as usize] = Value::Concrete(self.program_break);
} else {
self.program_break = new_program_break;
}
trace!(
"brk: old={:#x} new={:#x}",
old_program_break,
new_program_break
);
Ok(())
} else {
not_supported("can not handle symbolic or uninitialized program break")
}
}
fn bytewise_combine(
&mut self,
old: Value,
n_lower_bytes: u32,
new_idx: SymbolicValue,
) -> SymbolicValue {
let bits_in_a_byte = 8;
let low_shift_factor = 2_u64.pow(n_lower_bytes * bits_in_a_byte);
let high_shift_factor =
2_u64.pow((size_of::<u64>() as u32 - n_lower_bytes) * bits_in_a_byte);
assert!(
low_shift_factor != 0 && high_shift_factor != 0,
"no bytes to shift"
);
let old_idx = match old {
Value::Concrete(c) => {
let old_c = c / low_shift_factor * low_shift_factor;
self.symbolic_state.create_const(old_c)
}
Value::Symbolic(old_idx) => {
let low_shift_factor_idx = self.symbolic_state.create_const(low_shift_factor);
let old_idx = self.symbolic_state.create_operator(
BVOperator::Divu,
old_idx,
low_shift_factor_idx,
);
self.symbolic_state
.create_operator(BVOperator::Mul, old_idx, low_shift_factor_idx)
}
Value::Uninitialized => {
unreachable!("function should not be called for uninitialized values")
}
};
let high_shift_factor_idx = self.symbolic_state.create_const(high_shift_factor);
let new_idx =
self.symbolic_state
.create_operator(BVOperator::Mul, new_idx, high_shift_factor_idx);
let new_idx =
self.symbolic_state
.create_operator(BVOperator::Divu, new_idx, high_shift_factor_idx);
self.symbolic_state
.create_operator(BVOperator::Add, old_idx, new_idx)
}
fn execute_openat(&mut self) -> Result<(), SymbolicExecutionError> {
let dirfd = if let Value::Concrete(d) = self.regs[Register::A0 as usize] {
d
} else {
return not_supported("can only handle concrete values for dirfd in openat syscall");
};
let pathname = if let Value::Concrete(p) = self.regs[Register::A1 as usize] {
p
} else {
return not_supported("can only handle concrete values for pathname in openat syscall");
};
let flags = if let Value::Concrete(f) = self.regs[Register::A2 as usize] {
f
} else {
return not_supported("can only handle concrete values for flags in openat syscall");
};
let mode = if let Value::Concrete(m) = self.regs[Register::A3 as usize] {
m
} else {
return not_supported("can only handle concrete values for mode in openat syscall");
};
trace!(
"openat: dirfd={} pathname={} flags={} mode={}",
dirfd,
pathname,
flags,
mode
);
self.regs[Register::A0 as usize] = Value::Concrete(self.amount_of_file_descriptors);
self.amount_of_file_descriptors += 1;
Ok(())
}
fn execute_read(&mut self) -> Result<(), SymbolicExecutionError> {
if !matches!(self.regs[Register::A0 as usize], Value::Concrete(0)) {
return not_supported("can not handle fd other than stdin in read syscall");
}
let buffer = if let Value::Concrete(b) = self.regs[Register::A1 as usize] {
b
} else {
return not_supported(
"can not handle symbolic or uninitialized buffer address in read syscall",
);
};
let size = if let Value::Concrete(s) = self.regs[Register::A2 as usize] {
s
} else {
return not_supported("can not handle symbolic or uinitialized size in read syscall");
};
trace!("read: fd={} buffer={:#x} size={}", 0, buffer, size,);
self.check_for_valid_memory_range("read", buffer, size)?;
let size_of_u64 = size_of::<u64>() as u64;
let round_up = if size % size_of_u64 == 0 {
0
} else {
size_of_u64 - size % size_of_u64
};
let mut bytes_to_read = size;
let words_to_read = (bytes_to_read + round_up) / size_of_u64;
let start = buffer / size_of_u64;
for word_count in 0..words_to_read {
let start_byte = word_count * size_of_u64;
let end_byte = start_byte
+ if bytes_to_read < size_of_u64 {
bytes_to_read
} else {
8
};
let name = format!(
"read({}, {}, {})[{} - {}]",
0, buffer, size, start_byte, end_byte,
);
let input_idx = self.symbolic_state.create_input(&name);
let addr = (start + word_count) as usize;
let result_idx = if bytes_to_read >= size_of_u64 {
bytes_to_read -= size_of_u64;
input_idx
} else {
match self.memory[addr] {
Value::Uninitialized => {
break;
}
v => self.bytewise_combine(v, bytes_to_read as u32, input_idx),
}
};
self.memory[addr] = Value::Symbolic(result_idx);
}
self.regs[Register::A0 as usize] = Value::Concrete(size);
Ok(())
}
fn execute_write(&mut self) -> Result<(), SymbolicExecutionError> {
if !matches!(self.regs[Register::A0 as usize], Value::Concrete(1)) {
return not_supported("can not handle fd other than stdout in write syscall");
}
let buffer = if let Value::Concrete(b) = self.regs[Register::A1 as usize] {
b
} else {
return not_supported(
"can not handle symbolic or uninitialized buffer address in write syscall",
);
};
let size = if let Value::Concrete(s) = self.regs[Register::A2 as usize] {
s
} else {
return not_supported("can not handle symbolic or uinitialized size in write syscall");
};
trace!("write: fd={} buffer={:#x} size={}", 1, buffer, size,);
self.check_for_valid_memory_range("write", buffer, size)?;
let size_of_u64 = size_of::<u64>() as u64;
let start = buffer / size_of_u64;
let bytes_to_read = size + buffer % size_of_u64;
let words_to_read = (bytes_to_read + size_of_u64 - 1) / size_of_u64;
for word_count in 0..words_to_read {
let address = start + word_count;
if self.memory[address as usize] == Value::Uninitialized {
trace!(
"write: access to uninitialized memory at {:#x} => computing reachability",
(start + word_count) * size_of_u64,
);
return self.execute_query(Query::Reachable).and_then(|r| {
self.exit_anyway_with_bug(r, |i| {
self.access_to_uninitialized_memory_bug(
i,
UninitializedMemoryAccessReason::ReadUnintializedMemoryAddress {
description: format!(
"access to uninitialized memory at address: {:#x}",
address
),
address,
},
)
})
});
}
}
self.regs[Register::A0 as usize] = Value::Concrete(size);
Ok(())
}
fn should_execute_branch(&mut self) -> Result<(bool, &'static str), SymbolicExecutionError> {
Ok(match self.execute_query(Query::Reachable)? {
QueryResult::Sat(_) => (true, "reachable"),
QueryResult::Unknown if !self.options.optimistically_prune_search_space => {
(true, "reachability unknown")
}
_ => (false, "unreachable"),
})
}
fn with_snapshot<F, R>(&mut self, f: F) -> R
where
F: FnOnce(&mut Self) -> R,
{
let memory_snapshot = self.memory.clone();
let regs_snapshot = self.regs;
let graph_snapshot = Box::new((*self.symbolic_state).clone());
let brk_snapshot = self.program_break;
let execution_depth_snapshot = self.execution_depth;
let amount_of_file_descriptors_snapshot = self.amount_of_file_descriptors;
let result = f(self);
self.memory = memory_snapshot;
self.regs = regs_snapshot;
self.symbolic_state = graph_snapshot;
self.program_break = brk_snapshot;
self.execution_depth = execution_depth_snapshot;
self.amount_of_file_descriptors = amount_of_file_descriptors_snapshot;
result
}
fn execute_beq_branches(
&mut self,
true_branch: u64,
false_branch: u64,
lhs: SymbolicValue,
rhs: SymbolicValue,
) -> Result<(), SymbolicExecutionError> {
let next_pc = self.strategy.choose_path(true_branch, false_branch);
let decision = next_pc == true_branch;
let result_first_branch =
self.with_snapshot(|this| -> Result<(), SymbolicExecutionError> {
this.symbolic_state
.create_beq_path_condition(decision, lhs, rhs);
let (execute_branch, reachability) = this.should_execute_branch()?;
if execute_branch {
trace!(
"[{:#010x}] beq: x{}, x{} |- assume {} ({}), pc <- {:#x}",
this.pc,
lhs.index(),
rhs.index(),
next_pc == false_branch,
reachability,
next_pc,
);
this.pc = next_pc;
this.run()
} else {
trace!(
"[{:#010x}] beq: x{}, x{} |- assume {} ({})",
this.pc,
lhs.index(),
rhs.index(),
next_pc == false_branch,
reachability
);
Err(SymbolicExecutionError::NotReachable)
}
});
match result_first_branch {
Ok(_) => panic!("every branch execution has to end with an error"),
Err(SymbolicExecutionError::ExecutionDepthReached(_))
| Err(SymbolicExecutionError::ProgramExit(_))
| Err(SymbolicExecutionError::NotReachable) => {}
err => {
return err;
}
};
let next_pc = if decision { false_branch } else { true_branch };
self.symbolic_state
.create_beq_path_condition(!decision, lhs, rhs);
let (execute_branch, reachability) = self.should_execute_branch()?;
if execute_branch {
trace!(
"[{:#010x}] beq: x{}, x{} |- assume {} ({}), pc <- {:#x}",
self.pc,
lhs.index(),
rhs.index(),
next_pc == false_branch,
reachability,
next_pc,
);
self.pc = next_pc;
Ok(())
} else {
trace!(
"[{:#010x}] beq: x{}, x{} |- assume {} ({})",
self.pc,
lhs.index(),
rhs.index(),
next_pc == false_branch,
reachability
);
result_first_branch
}
}
fn execute_beq(&mut self, btype: BType) -> Result<(), SymbolicExecutionError> {
let lhs = self.regs[btype.rs1() as usize];
let rhs = self.regs[btype.rs2() as usize];
let true_branch = self.pc.wrapping_add(btype.imm() as u64);
let false_branch = self.pc.wrapping_add(INSTRUCTION_SIZE);
match (lhs, rhs) {
(Value::Concrete(v1), Value::Concrete(v2)) => {
let old_pc = self.pc;
self.pc = if v1 == v2 { true_branch } else { false_branch };
trace!(
"[{:#010x}] beq: {}, {} |- pc <- {:#x}",
old_pc,
lhs,
rhs,
self.pc
);
Ok(())
}
(Value::Symbolic(v1), Value::Concrete(v2)) => {
let v2 = self.symbolic_state.create_const(v2);
self.execute_beq_branches(true_branch, false_branch, v1, v2)
}
(Value::Concrete(v1), Value::Symbolic(v2)) => {
let v1 = self.symbolic_state.create_const(v1);
self.execute_beq_branches(true_branch, false_branch, v1, v2)
}
(Value::Symbolic(v1), Value::Symbolic(v2)) => {
self.execute_beq_branches(true_branch, false_branch, v1, v2)
}
(v1, v2) => self.access_to_uninitialized_memory(Instruction::Beq(btype), v1, v2),
}
}
fn execute_exit(&mut self) -> Result<(), SymbolicExecutionError> {
match self.regs[Register::A0 as usize] {
Value::Symbolic(exit_code) => {
trace!("exit: symbolic code -> find input for exit_code != 0");
self.execute_query(Query::NotEquals((exit_code, 0)))
.and_then(|r| {
self.exit_anyway_with_bug_if_sat(
r,
|i| self.exit_code_greater_zero_bug(i, Value::Symbolic(exit_code)),
SymbolicExecutionError::ProgramExit(Value::Symbolic(exit_code)),
)
})
}
Value::Concrete(exit_code) => {
if exit_code > 0 {
trace!(
"exit: with code {} -> find input to satisfy path condition",
exit_code
);
self.execute_query(Query::Reachable).and_then(|r| {
self.exit_anyway_with_bug(r, |i| {
self.exit_code_greater_zero_bug(i, Value::Concrete(exit_code))
})
})
} else {
trace!("exiting context with exit_code 0");
Err(SymbolicExecutionError::ProgramExit(Value::Concrete(
exit_code,
)))
}
}
_ => not_supported("exit only implemented for symbolic exit codes"),
}
}
fn execute_ecall(&mut self) -> Result<(), SymbolicExecutionError> {
trace!("[{:#010x}] ecall", self.pc);
let result = match self.regs[Register::A7 as usize] {
Value::Concrete(syscall_id) if syscall_id == (SyscallId::Brk as u64) => {
self.execute_brk()
}
Value::Concrete(syscall_id) if syscall_id == (SyscallId::Openat as u64) => {
self.execute_openat()
}
Value::Concrete(syscall_id) if syscall_id == (SyscallId::Read as u64) => {
self.execute_read()
}
Value::Concrete(syscall_id) if syscall_id == (SyscallId::Write as u64) => {
self.execute_write()
}
Value::Concrete(syscall_id) if syscall_id == (SyscallId::Exit as u64) => {
self.execute_exit()
}
id => Err(SymbolicExecutionError::NotSupported(format!(
"syscall with id ({}) is not supported",
id
))),
};
self.pc += INSTRUCTION_SIZE;
result
}
fn execute_ld(
&mut self,
instruction: Instruction,
itype: IType,
) -> Result<(), SymbolicExecutionError> {
if let Value::Concrete(base_address) = self.regs[itype.rs1() as usize] {
let immediate = itype.imm() as u64;
let address = base_address.wrapping_add(immediate);
self.check_for_valid_memory_address(instruction_to_str(instruction), address)?;
let value = self.memory[(address / 8) as usize];
trace!(
"[{:#010x}] {}: {:#x}, {} |- {:?} <- mem[{:#x}]={}",
self.pc,
instruction_to_str(instruction),
base_address,
immediate,
itype.rd(),
address,
value,
);
self.assign_rd(itype.rd(), value);
self.pc += INSTRUCTION_SIZE;
Ok(())
} else {
not_supported("can not handle symbolic addresses in LD")
}
}
fn execute_sd(
&mut self,
instruction: Instruction,
stype: SType,
) -> Result<(), SymbolicExecutionError> {
if let Value::Concrete(base_address) = self.regs[stype.rs1() as usize] {
let immediate = stype.imm();
let address = base_address.wrapping_add(immediate as u64);
self.check_for_valid_memory_address(instruction_to_str(instruction), address)?;
let value = self.regs[stype.rs2() as usize];
trace!(
"[{:#010x}] {}: {:#x}, {}, {} |- mem[{:#x}] <- {}",
self.pc,
instruction_to_str(instruction),
base_address,
immediate,
self.regs[stype.rs2() as usize],
address,
value,
);
self.memory[(address / 8) as usize] = value;
self.pc += INSTRUCTION_SIZE;
Ok(())
} else {
not_supported("can not handle symbolic addresses in SD")
}
}
#[allow(clippy::unnecessary_wraps)]
fn execute_jal(&mut self, jtype: JType) -> Result<(), SymbolicExecutionError> {
let link = self.pc + INSTRUCTION_SIZE;
let new_pc = self.pc.wrapping_add(jtype.imm() as u64);
trace!(
"[{:#010x}] jal: pc <- {:#x}, {:?} <- {:#x}",
self.pc,
new_pc,
jtype.rd(),
link,
);
self.pc = new_pc;
self.assign_rd(jtype.rd(), Value::Concrete(link));
Ok(())
}
fn assign_rd(&mut self, rd: Register, v: Value) {
if rd != Register::Zero {
self.regs[rd as usize] = v;
}
}
fn execute_jalr(&mut self, itype: IType) -> Result<(), SymbolicExecutionError> {
if let Value::Concrete(dest) = self.regs[itype.rs1() as usize] {
let link = self.pc + INSTRUCTION_SIZE;
let new_pc = dest.wrapping_add(itype.imm() as u64);
trace!(
"[{:#010x}] jalr: {:#x}, {} |- pc <- {:#x}, {:?} <- {:#x}",
self.pc,
dest,
itype.imm(),
new_pc,
itype.rd(),
link
);
self.assign_rd(itype.rd(), Value::Concrete(link));
self.pc = new_pc;
Ok(())
} else {
not_supported("can only handle concrete addresses in JALR")
}
}
fn fetch(&self) -> Result<u32, SymbolicExecutionError> {
if let Value::Concrete(dword) = self.memory[(self.pc as usize / size_of::<u64>()) as usize]
{
if self.pc % size_of::<u64>() as u64 == 0 {
Ok(dword as u32)
} else {
Ok((dword >> 32) as u32)
}
} else {
Err(SymbolicExecutionError::NotSupported(String::from(
"tried to fetch none concrete instruction",
)))
}
}
fn execute(&mut self, instruction: Instruction) -> Result<(), SymbolicExecutionError> {
match 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),
Instruction::Sub(rtype) => self.execute_rtype(instruction, rtype, u64::wrapping_sub),
Instruction::Mul(rtype) => self.execute_rtype(instruction, rtype, u64::wrapping_mul),
Instruction::Divu(rtype) => {
self.execute_divu_remu(instruction, rtype, u64::wrapping_div)
}
Instruction::Remu(rtype) => {
self.execute_divu_remu(instruction, rtype, u64::wrapping_rem)
}
Instruction::Sltu(rtype) => {
self.execute_rtype(instruction, rtype, |l, r| if l < r { 1 } else { 0 })
}
Instruction::Ld(itype) => self.execute_ld(instruction, itype),
Instruction::Sd(stype) => self.execute_sd(instruction, stype),
Instruction::Jal(jtype) => self.execute_jal(jtype),
Instruction::Jalr(itype) => self.execute_jalr(itype),
Instruction::Beq(btype) => self.execute_beq(btype),
}
}
}
fn load_segment(memory: &mut Vec<Value>, segment: &ProgramSegment<u8>) {
let start = segment.address as usize / size_of::<u64>();
let end = start + segment.content.len() / size_of::<u64>();
segment
.content
.chunks(size_of::<u64>())
.map(LittleEndian::read_u64)
.zip(start..end)
.for_each(|(x, i)| memory[i] = Value::Concrete(x));
}
fn not_supported(s: &str) -> Result<(), SymbolicExecutionError> {
Err(SymbolicExecutionError::NotSupported(s.to_owned()))
}
#[derive(Debug, Clone)]
pub struct SymbolicExecutionBugInfo {
pub witness: Option<Witness>,
pub pc: u64,
}
impl BugInfo for SymbolicExecutionBugInfo {
type Value = Value;
}
impl fmt::Display for SymbolicExecutionBugInfo {
fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
write!(f, "pc: {:#010x}", self.pc)?;
if let Some(witness) = &self.witness {
write!(f, "\nwitness: {}", witness)
} else {
Ok(())
}
}
}