Skip to content

Commit

Permalink
(isla-axiomatic/smt) don't generate trivial bitvector constraints
Browse files Browse the repository at this point in the history
  • Loading branch information
@bensimner
bensimner committed Jun 11, 2024
1 parent 6af9c9d commit afe3449
Show file tree
Hide file tree
Showing 2 changed files with 73 additions and 52 deletions.
104 changes: 52 additions & 52 deletions isla-axiomatic/src/smt_events.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -72,7 +72,7 @@ fn same_location<B: BV>(ev1: &AxEvent<B>, ev2: &AxEvent<B>) -> Sexp {
if bv1 == bv2 {
True
} else {
Literal(format!("(= {} {})", bv1, bv2))
False
}
}
(_, _) => False,
Expand Down Expand Up @@ -101,7 +101,7 @@ fn overlap_location<B: BV>(ev1: &AxEvent<B>, ev2: &AxEvent<B>) -> Sexp {
if bv1 == bv2 {
checks.push(True)
} else {
checks.push(Literal(format!("(= {} {})", bv1, bv2)))
checks.push(False)
}
}
(_, _) => checks.push(False),
Expand Down Expand Up @@ -160,80 +160,78 @@ fn read_initial_symbolic<B: BV>(
memory: &Memory<B>,
initial_addrs: &HashMap<u64, u64>,
) -> Sexp {
let mut expr = "".to_string();
let mut ites = 0;
use Sexp::*;

for (addr2, value) in initial_addrs {
expr = format!(
"{}(ite (= {} {}) (= v{} {}) ",
expr,
smt_bitvec(addr1),
B::new(*addr2, 64),
sym,
B::new(*value, 8 * bytes)
);
ites += 1
}
let sym = Val::Symbolic::<B>(sym);

let region_info = if let Val::Bits(concrete_addr) = addr1 {
memory.in_custom_region(concrete_addr.lower_u64()).map(|region| (region, concrete_addr.lower_u64()))
} else {
None
};

if let Some((region, concrete_addr)) = region_info {
if let Some(bv) = region.initial_value(concrete_addr, bytes) {
expr = format!("{}(= v{} {})", expr, sym, bv);
} else {
expr = format!("{}(= v{} {})", expr, sym, B::new(0, 8 * bytes));
}
} else {
expr = format!("{}(= v{} {})", expr, sym, B::new(0, 8 * bytes));
}
let mut expr = {
let bv =
if let Some((region, concrete_addr)) = region_info {
match region.initial_value(concrete_addr, bytes) {
Some(bv) => bv,
None => B::new(0, 8 * bytes),
}
} else {
B::new(0, 8 * bytes)
};
let bv = Val::Bits(bv);
Eq(Box::new(Literal(smt_bitvec(&sym))), Box::new(Literal(smt_bitvec(&bv))))
};

for _ in 0..ites {
expr = format!("{})", expr)
for (addr2, value) in initial_addrs {
let addr2 = Val::Bits(B::new(*addr2, 64));
let value = Val::Bits(B::new(*value, 8 * bytes));

expr = IfThenElse(
Box::new(Eq(Box::new(Literal(smt_bitvec(addr1))), Box::new(Literal(smt_bitvec(&addr2))))),
Box::new(Eq(Box::new(Literal(smt_bitvec(&value))), Box::new(Literal(smt_bitvec(&sym))))),
Box::new(expr),
);
}

Sexp::Literal(expr)
expr
}

fn read_initial_concrete<B: BV>(bv: B, addr1: &Val<B>, memory: &Memory<B>, initial_addrs: &HashMap<u64, u64>) -> Sexp {
let mut expr = "".to_string();
let mut ites = 0;

for (addr2, value) in initial_addrs {
expr = format!(
"{}(ite (= {} {}) {} ",
expr,
smt_bitvec(addr1),
B::new(*addr2, 64),
if bv.lower_u64() == *value { "true" } else { "false " }
);
ites += 1
}
use Sexp::*;

let region_info = if let Val::Bits(concrete_addr) = addr1 {
memory.in_custom_region(concrete_addr.lower_u64()).map(|region| (region, concrete_addr.lower_u64()))
} else {
None
};

if let Some((region, concrete_addr)) = region_info {
expr = format!(
"{}{}",
expr,
if Some(bv) == region.initial_value(concrete_addr, bv.len() / 8) { "true" } else { "false" }
);
} else {
expr = format!("{}{}", expr, if bv.is_zero() { "true" } else { "false" });
}
let mut expr =
if let Some((region, concrete_addr)) = region_info {
if Some(bv) == region.initial_value(concrete_addr, bv.len() / 8) {
True
} else {
False
}
} else {
if bv.is_zero() {
True
} else {
False
}
};

for _ in 0..ites {
expr = format!("{})", expr)
for (addr2, value) in initial_addrs {
let addr2 = Val::Bits(B::new(*addr2, 64));
expr = IfThenElse(
Box::new(Eq(Box::new(Literal(smt_bitvec(addr1))), Box::new(Literal(smt_bitvec(&addr2))))),
Box::new(if bv.lower_u64() == *value { True } else { False }),
Box::new(expr),
);
}

Sexp::Literal(expr)
expr
}

fn initial_write_values<B: BV>(addr_name: &str, width: u32, initial_addrs: &HashMap<u64, u64>) -> String {
Expand Down Expand Up @@ -414,6 +412,7 @@ where
f(ev1, ev2),
]))
}
deps.push(False);
let mut sexp = Or(deps);
sexp.simplify(&HashSet::new());
sexp
Expand Down Expand Up @@ -481,6 +480,7 @@ where
for ev in events.iter() {
deps.push(And(vec![Eq(Box::new(Var(1)), Box::new(Literal(ev.name.to_string()))), set(ev)]))
}
deps.push(False);
let mut sexp = Or(deps);
sexp.simplify(&HashSet::new());
sexp
Expand Down
21 changes: 21 additions & 0 deletions isla-cat/src/smt.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -65,6 +65,7 @@ pub enum Sexp {
Or(Vec<Sexp>),
And(Vec<Sexp>),
Not(Box<Sexp>),
IfThenElse(Box<Sexp>, Box<Sexp>, Box<Sexp>),
Eq(Box<Sexp>, Box<Sexp>),
Exists(EventId, Box<Sexp>),
Implies(Box<Sexp>, Box<Sexp>),
Expand All @@ -87,6 +88,11 @@ impl Sexp {
Implies(sexp1, sexp2) | Eq(sexp1, sexp2) => {
sexp1.modify(f);
sexp2.modify(f)
},
IfThenElse(sexp1, sexp2, sexp3) => {
sexp1.modify(f);
sexp2.modify(f);
sexp3.modify(f)
}
And(sexps) | Or(sexps) => sexps.iter_mut().for_each(|sexp| sexp.modify(f)),
}
Expand Down Expand Up @@ -161,6 +167,14 @@ impl Sexp {
}
}

IfThenElse(sexp1, sexp2, sexp3) => {
if sexp1.is_true() {
*self = *sexp2.clone();
} else if sexp1.is_false() {
*self = *sexp3.clone();
}
}

Not(sexp) => match &**sexp {
Not(sexp) => *self = (**sexp).clone(),
True => *self = False,
Expand Down Expand Up @@ -256,6 +270,13 @@ impl Sexp {
}
write!(output, ")")?
}
IfThenElse(sexp1, sexp2, sexp3) => {
writeln!(output, "(ite ")?;
sexp1.write_to(output, true, amount + 2, true)?;
sexp2.write_to(output, true, amount + 2, true)?;
sexp3.write_to(output, true, amount + 2, false)?;
write!(output, ")")?
}
Implies(sexp1, sexp2) => {
write!(output, "(=> ")?;
sexp1.write_to(output, false, amount + 4, true)?;
Expand Down

0 comments on commit afe3449

Please sign in to comment.