Skip to content

Commit

Permalink
fix: fold all constants in SMT query (#100) (#101)
Browse files Browse the repository at this point in the history 
* fix: fold all constants in SMT query (#100)

closes #100

* fix: disallow division by zero with a constraint (#102) (#103)

closes #102
  • Loading branch information
@ChristianMoesl
ChristianMoesl authored Dec 10, 2020
1 parent 867a240 commit a2dfc0a
Show file tree
Hide file tree
Showing 6 changed files with 172 additions and 120 deletions.
23 changes: 11 additions & 12 deletions src/boolector.rs
View file
Original file line number Diff line number Diff line change
@@ -1,17 +1,17 @@
use crate::bitvec::BitVector;
use crate::engine::EngineError;
use crate::solver::{Assignment, Solver};
use crate::symbolic_state::{
get_operands, BVOperator, Formula,
Node::{Constant, Input, Operator},
SymbolId,
use crate::{
bitvec::BitVector,
solver::{Assignment, Solver, SolverError},
symbolic_state::{
get_operands, BVOperator, Formula,
Node::{Constant, Input, Operator},
SymbolId,
},
};
use boolector::{
option::{BtorOption, ModelGen, OutputFileFormat},
Btor, SolverResult, BV,
};
use std::collections::HashMap;
use std::rc::Rc;
use std::{collections::HashMap, rc::Rc};

pub struct Boolector {}

Expand All @@ -36,7 +36,7 @@ impl Solver for Boolector {
&self,
graph: &Formula,
root: SymbolId,
) -> Result<Option<Assignment<BitVector>>, EngineError> {
) -> Result<Option<Assignment<BitVector>>, SolverError> {
let solver = Rc::new(Btor::new());
solver.set_opt(BtorOption::ModelGen(ModelGen::All));
solver.set_opt(BtorOption::Incremental(true));
Expand All @@ -50,7 +50,6 @@ impl Solver for Boolector {
SolverResult::Sat => {
let assignments = graph
.node_indices()
//.filter(|i| matches!(graph[*i], Input(_)))
.map(|i| {
let bv = bvs.get(&i).expect("every input must be part of bvs");

Expand All @@ -65,7 +64,7 @@ impl Solver for Boolector {
Ok(Some(assignments))
}
SolverResult::Unsat => Ok(None),
SolverResult::Unknown => Ok(None),
SolverResult::Unknown => Err(SolverError::SatUnknown),
}
}
}
Expand Down
60 changes: 31 additions & 29 deletions src/engine.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,8 +3,8 @@ use crate::{
bug::{BasicInfo, Bug},
cfg::build_cfg_from_file,
exploration_strategy::{ExplorationStrategy, ShortestPathStrategy},
solver::{MonsterSolver, Solver},
symbolic_state::{BVOperator, Query, QueryError, SymbolId, SymbolicState},
solver::{MonsterSolver, Solver, SolverError},
symbolic_state::{BVOperator, Query, SymbolId, SymbolicState},
z3::Z3,
};
use byteorder::{ByteOrder, LittleEndian};
Expand Down Expand Up @@ -108,10 +108,7 @@ pub enum EngineError {
InvalidInstructionEncoding(u64, DecodingError),

#[error("failed to compute satisfyability for formula")]
SatUnknown(QueryError),

#[error("could not find a satisfiable assignment before timing out")]
SatTimeout(),
SatUnknown(SolverError),
}

pub struct Engine<'a, E, S>
Expand Down Expand Up @@ -233,8 +230,7 @@ where
Ok(self
.symbolic_state
.execute_query(query)
// TODO: differenciate between unsat, timeout and error
//.map_err(|e| EngineError::SatUnknown(e))
.map_err(EngineError::SatUnknown)
.map_or(None, |result| {
result.map(|witness| {
basic_info_to_bug(BasicInfo {
Expand Down Expand Up @@ -460,26 +456,39 @@ where
}
}

fn bytewise_combine(
&mut self,
old_idx: SymbolId,
n_lower_bytes: u32,
new_idx: SymbolId,
) -> SymbolId {
fn bytewise_combine(&mut self, old: Value, n_lower_bytes: u32, new_idx: SymbolId) -> SymbolId {
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);

let low_shift_factor_idx = self.symbolic_state.create_const(low_shift_factor);
assert!(
low_shift_factor != 0 && high_shift_factor != 0,
"no bytes to shift"
);

let old_idx =
self.symbolic_state
.create_operator(BVOperator::Divu, old_idx, low_shift_factor_idx);
let old_idx = match old {
Value::Concrete(c) => {
let old_c = c / low_shift_factor * low_shift_factor;

let old_idx =
self.symbolic_state
.create_operator(BVOperator::Mul, old_idx, low_shift_factor_idx);
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);

Expand Down Expand Up @@ -560,14 +569,7 @@ where
// if at least one byte in a word is uninitialized, the whole word is uninitialized
break;
}
Value::Symbolic(old_idx) => {
self.bytewise_combine(old_idx, bytes_to_read as u32, input_idx)
}
Value::Concrete(c) => {
let old_idx = self.symbolic_state.create_const(c);

self.bytewise_combine(old_idx, bytes_to_read as u32, input_idx)
}
v => self.bytewise_combine(v, bytes_to_read as u32, input_idx),
}
};

Expand Down
36 changes: 26 additions & 10 deletions src/solver.rs
View file
Original file line number Diff line number Diff line change
@@ -1,13 +1,15 @@
#![allow(clippy::many_single_char_names)]

use crate::bitvec::*;
use crate::engine::EngineError;
use crate::symbolic_state::{get_operands, BVOperator, Formula, Node, OperandSide, SymbolId};
use crate::ternary::*;
use crate::{
bitvec::*,
symbolic_state::{get_operands, BVOperator, Formula, Node, OperandSide, SymbolId},
ternary::*,
};
use log::{debug, log_enabled, trace, Level};
use petgraph::{visit::EdgeRef, Direction};
use rand::{distributions::Uniform, random, thread_rng, Rng};
use std::time::{Duration, Instant};
use thiserror::Error;

pub type Assignment<T> = Vec<T>;

Expand All @@ -18,7 +20,7 @@ pub trait Solver: Default {
&self,
formula: &Formula,
root: SymbolId,
) -> Result<Option<Assignment<BitVector>>, EngineError> {
) -> Result<Option<Assignment<BitVector>>, SolverError> {
debug!("try to solve with {} solver", Self::name());

time_debug!("finished solving formula", {
Expand All @@ -30,7 +32,16 @@ pub trait Solver: Default {
&self,
formula: &Formula,
root: SymbolId,
) -> Result<Option<Assignment<BitVector>>, EngineError>;
) -> Result<Option<Assignment<BitVector>>, SolverError>;
}

#[derive(Debug, Error)]
pub enum SolverError {
#[error("failed to compute satisfiability within the given limits")]
SatUnknown,

#[error("could not find a satisfiable assignment before timing out")]
Timeout,
}

pub struct MonsterSolver {}
Expand All @@ -56,11 +67,11 @@ impl Solver for MonsterSolver {
&self,
formula: &Formula,
root: SymbolId,
) -> Result<Option<Assignment<BitVector>>, EngineError> {
) -> Result<Option<Assignment<BitVector>>, SolverError> {
let ab = initialize_ab(formula);
let at = compute_at(formula);

let timeout_time = Duration::new(20, 0);
let timeout_time = Duration::new(3, 0);

sat(formula, root, at, ab, timeout_time)
}
Expand Down Expand Up @@ -522,6 +533,11 @@ fn get_operand(f: &Formula, n: SymbolId) -> SymbolId {
fn update_assignment(f: &Formula, ab: &mut Assignment<BitVector>, n: SymbolId, v: BitVector) {
ab[n.index()] = v;

assert!(
matches!(f[n], Node::Input(_)),
"only inputs can be assigned"
);

trace!("update: x{} <- {:#x}", n.index(), v.0);

f.neighbors_directed(n, Direction::Outgoing)
Expand Down Expand Up @@ -621,7 +637,7 @@ fn sat(
at: Assignment<TernaryBitVector>,
mut ab: Assignment<BitVector>,
timeout_time: Duration,
) -> Result<Option<Assignment<BitVector>>, EngineError> {
) -> Result<Option<Assignment<BitVector>>, SolverError> {
let mut iterations = 0;

let start_time = Instant::now();
Expand All @@ -635,7 +651,7 @@ fn sat(

while !is_leaf(formula, n) {
if start_time.elapsed() > timeout_time {
return Err(EngineError::SatTimeout());
return Err(SolverError::Timeout);
}
let (v, nx) = match formula[n] {
Node::Operator(op) => {
Expand Down
Loading

0 comments on commit a2dfc0a

Please sign in to comment.