From afe34497ecffe36a7528e4d7fec40e221f3d3157 Mon Sep 17 00:00:00 2001 From: Ben Simner Date: Tue, 4 Jun 2024 09:20:49 +0000 Subject: [PATCH] (isla-axiomatic/smt) don't generate trivial bitvector constraints --- isla-axiomatic/src/smt_events.rs | 104 +++++++++++++++---------------- isla-cat/src/smt.rs | 21 +++++++ 2 files changed, 73 insertions(+), 52 deletions(-) diff --git a/isla-axiomatic/src/smt_events.rs b/isla-axiomatic/src/smt_events.rs index dc3f39b..2256dc9 100644 --- a/isla-axiomatic/src/smt_events.rs +++ b/isla-axiomatic/src/smt_events.rs @@ -72,7 +72,7 @@ fn same_location(ev1: &AxEvent, ev2: &AxEvent) -> Sexp { if bv1 == bv2 { True } else { - Literal(format!("(= {} {})", bv1, bv2)) + False } } (_, _) => False, @@ -101,7 +101,7 @@ fn overlap_location(ev1: &AxEvent, ev2: &AxEvent) -> Sexp { if bv1 == bv2 { checks.push(True) } else { - checks.push(Literal(format!("(= {} {})", bv1, bv2))) + checks.push(False) } } (_, _) => checks.push(False), @@ -160,20 +160,9 @@ fn read_initial_symbolic( memory: &Memory, initial_addrs: &HashMap, ) -> 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::(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())) @@ -181,37 +170,36 @@ fn read_initial_symbolic( 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(bv: B, addr1: &Val, memory: &Memory, initial_addrs: &HashMap) -> 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())) @@ -219,21 +207,31 @@ fn read_initial_concrete(bv: B, addr1: &Val, memory: &Memory, initi 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(addr_name: &str, width: u32, initial_addrs: &HashMap) -> String { @@ -414,6 +412,7 @@ where f(ev1, ev2), ])) } + deps.push(False); let mut sexp = Or(deps); sexp.simplify(&HashSet::new()); sexp @@ -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 diff --git a/isla-cat/src/smt.rs b/isla-cat/src/smt.rs index 2ba37e1..d4b0b67 100644 --- a/isla-cat/src/smt.rs +++ b/isla-cat/src/smt.rs @@ -65,6 +65,7 @@ pub enum Sexp { Or(Vec), And(Vec), Not(Box), + IfThenElse(Box, Box, Box), Eq(Box, Box), Exists(EventId, Box), Implies(Box, Box), @@ -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)), } @@ -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, @@ -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)?;