Skip to content

C
cwe_checker
Unverified Commit 36af53ad by Enkelmann Committed by GitHub
Options

Refactor the state module for cleaner code (#224)

parent 05843314
Showing with 478 additions and 464 deletions
src/cwe_checker_lib/src/analysis/pointer_inference/state/access_handling.rs
//! Methods of [`State`] for handling memory and register access operations.
use crate::utils::binary::RuntimeMemoryImage;
use super::*;
......
src/cwe_checker_lib/src/analysis/pointer_inference/state/id_manipulation.rs 0 → 100644
//! Methods of [`State`] for manipulating abstract IDs.
use super::*;
impl State {
/// Replace all occurences of old_id with new_id and adjust offsets accordingly.
/// This is needed to replace stack/caller IDs on call and return instructions.
///
/// **Example:**
/// Assume the old_id points to offset 0 in the corresponding memory object and the new_id points to offset -32.
/// Then the offset_adjustment is -32.
/// The offset_adjustment gets *added* to the base offset in self.memory.ids (so that it points to offset -32 in the memory object),
/// while it gets *subtracted* from all pointer values (so that they still point to the same spot in the corresponding memory object).
pub fn replace_abstract_id(
&mut self,
old_id: &AbstractIdentifier,
new_id: &AbstractIdentifier,
offset_adjustment: &ValueDomain,
) {
for register_data in self.register.values_mut() {
register_data.replace_abstract_id(old_id, new_id, &(-offset_adjustment.clone()));
}
self.memory
.replace_abstract_id(old_id, new_id, offset_adjustment);
if &self.stack_id == old_id {
self.stack_id = new_id.clone();
}
if self.caller_stack_ids.get(old_id).is_some() {
self.caller_stack_ids.remove(old_id);
self.caller_stack_ids.insert(new_id.clone());
}
if self.ids_known_to_caller.get(old_id).is_some() {
self.ids_known_to_caller.remove(old_id);
self.ids_known_to_caller.insert(new_id.clone());
}
}
/// Search (recursively) through all memory objects referenced by the given IDs
/// and add all IDs reachable through concrete pointers contained in them to the set of IDs.
///
/// This uses an underapproximation of the referenced IDs of a memory object,
/// i.e. IDs may be missing if the analysis lost track of the corresponding pointer.
pub fn add_directly_reachable_ids_to_id_set(
&self,
mut ids: BTreeSet<AbstractIdentifier>,
) -> BTreeSet<AbstractIdentifier> {
let mut unsearched_ids = ids.clone();
while let Some(id) = unsearched_ids.iter().next() {
let id = id.clone();
unsearched_ids.remove(&id);
let memory_ids = self.memory.get_referenced_ids_underapproximation(&id);
for mem_id in memory_ids {
if ids.get(&mem_id).is_none() {
ids.insert(mem_id.clone());
unsearched_ids.insert(mem_id.clone());
}
}
}
ids
}
/// Search (recursively) through all memory objects referenced by the given IDs
/// and add all IDs contained in them to the set of IDs.
///
/// This uses an overapproximation of the referenced IDs of a memory object,
/// i.e. for a memory object it may add IDs as possible references
/// where the corresponding reference is not longer present in the memory object.
pub fn add_recursively_referenced_ids_to_id_set(
&self,
mut ids: BTreeSet<AbstractIdentifier>,
) -> BTreeSet<AbstractIdentifier> {
let mut unsearched_ids = ids.clone();
while let Some(id) = unsearched_ids.iter().next() {
let id = id.clone();
unsearched_ids.remove(&id);
let memory_ids = self.memory.get_referenced_ids_overapproximation(&id);
for mem_id in memory_ids {
if ids.get(&mem_id).is_none() {
ids.insert(mem_id.clone());
unsearched_ids.insert(mem_id.clone());
}
}
}
ids
}
/// Recursively remove all `caller_stack_ids` not corresponding to the given caller.
pub fn remove_other_caller_stack_ids(&mut self, caller_id: &AbstractIdentifier) {
let mut ids_to_remove = self.caller_stack_ids.clone();
ids_to_remove.remove(caller_id);
for register_value in self.register.values_mut() {
register_value.remove_ids(&ids_to_remove);
if register_value.is_empty() {
*register_value = register_value.top();
}
}
self.memory.remove_ids(&ids_to_remove);
self.caller_stack_ids = BTreeSet::new();
self.caller_stack_ids.insert(caller_id.clone());
self.ids_known_to_caller = self
.ids_known_to_caller
.difference(&ids_to_remove)
.cloned()
.collect();
}
}
src/cwe_checker_lib/src/analysis/pointer_inference/state/mod.rs
......@@ -7,6 +7,8 @@ use crate::utils::binary::RuntimeMemoryImage;
use std::collections::{BTreeMap, BTreeSet};
mod access_handling;
mod id_manipulation;
mod value_specialization;
/// Contains all information known about the state of a program at a specific point of time.
#[derive(Serialize, Deserialize, Debug, PartialEq, Eq, Clone)]
......@@ -139,38 +141,6 @@ impl State {
result_log
}
/// Replace all occurences of old_id with new_id and adjust offsets accordingly.
/// This is needed to replace stack/caller IDs on call and return instructions.
///
/// **Example:**
/// Assume the old_id points to offset 0 in the corresponding memory object and the new_id points to offset -32.
/// Then the offset_adjustment is -32.
/// The offset_adjustment gets *added* to the base offset in self.memory.ids (so that it points to offset -32 in the memory object),
/// while it gets *subtracted* from all pointer values (so that they still point to the same spot in the corresponding memory object).
pub fn replace_abstract_id(
&mut self,
old_id: &AbstractIdentifier,
new_id: &AbstractIdentifier,
offset_adjustment: &ValueDomain,
) {
for register_data in self.register.values_mut() {
register_data.replace_abstract_id(old_id, new_id, &(-offset_adjustment.clone()));
}
self.memory
.replace_abstract_id(old_id, new_id, offset_adjustment);
if &self.stack_id == old_id {
self.stack_id = new_id.clone();
}
if self.caller_stack_ids.get(old_id).is_some() {
self.caller_stack_ids.remove(old_id);
self.caller_stack_ids.insert(new_id.clone());
}
if self.ids_known_to_caller.get(old_id).is_some() {
self.ids_known_to_caller.remove(old_id);
self.ids_known_to_caller.insert(new_id.clone());
}
}
/// Remove all objects that cannot longer be reached by any known pointer.
/// This does not remove objects, where some caller may still know a pointer to the object.
///
......@@ -190,55 +160,6 @@ impl State {
self.memory.remove_unused_objects(&referenced_ids);
}
/// Search (recursively) through all memory objects referenced by the given IDs
/// and add all IDs reachable through concrete pointers contained in them to the set of IDs.
///
/// This uses an underapproximation of the referenced IDs of a memory object,
/// i.e. IDs may be missing if the analysis lost track of the corresponding pointer.
pub fn add_directly_reachable_ids_to_id_set(
&self,
mut ids: BTreeSet<AbstractIdentifier>,
) -> BTreeSet<AbstractIdentifier> {
let mut unsearched_ids = ids.clone();
while let Some(id) = unsearched_ids.iter().next() {
let id = id.clone();
unsearched_ids.remove(&id);
let memory_ids = self.memory.get_referenced_ids_underapproximation(&id);
for mem_id in memory_ids {
if ids.get(&mem_id).is_none() {
ids.insert(mem_id.clone());
unsearched_ids.insert(mem_id.clone());
}
}
}
ids
}
/// Search (recursively) through all memory objects referenced by the given IDs
/// and add all IDs contained in them to the set of IDs.
///
/// This uses an overapproximation of the referenced IDs of a memory object,
/// i.e. for a memory object it may add IDs as possible references
/// where the corresponding reference is not longer present in the memory object.
pub fn add_recursively_referenced_ids_to_id_set(
&self,
mut ids: BTreeSet<AbstractIdentifier>,
) -> BTreeSet<AbstractIdentifier> {
let mut unsearched_ids = ids.clone();
while let Some(id) = unsearched_ids.iter().next() {
let id = id.clone();
unsearched_ids.remove(&id);
let memory_ids = self.memory.get_referenced_ids_overapproximation(&id);
for mem_id in memory_ids {
if ids.get(&mem_id).is_none() {
ids.insert(mem_id.clone());
unsearched_ids.insert(mem_id.clone());
}
}
}
ids
}
/// Merge the callee stack with the caller stack.
///
/// This deletes the memory object corresponding to the callee_id
......@@ -284,26 +205,6 @@ impl State {
.collect();
}
/// Recursively remove all `caller_stack_ids` not corresponding to the given caller.
pub fn remove_other_caller_stack_ids(&mut self, caller_id: &AbstractIdentifier) {
let mut ids_to_remove = self.caller_stack_ids.clone();
ids_to_remove.remove(caller_id);
for register_value in self.register.values_mut() {
register_value.remove_ids(&ids_to_remove);
if register_value.is_empty() {
*register_value = register_value.top();
}
}
self.memory.remove_ids(&ids_to_remove);
self.caller_stack_ids = BTreeSet::new();
self.caller_stack_ids.insert(caller_id.clone());
self.ids_known_to_caller = self
.ids_known_to_caller
.difference(&ids_to_remove)
.cloned()
.collect();
}
/// Add those objects from the `caller_state` to `self`, that are not known to `self`.
///
/// Since self does not know these objects, we assume that the current function could not have accessed
......@@ -355,369 +256,6 @@ impl State {
self.register.remove(&register);
}
}
/// Try to restrict the input variables of `expression` on `self`
/// so that `expression` only evaluates to values represented by the given `result`.
///
/// If `expression` cannot evaluate to any value represented by `self`, return an error.
///
/// This function may restrict to upper bounds of possible values
/// if the restriction cannot be made exact,
/// i.e. after calling this function the state may still contain values
/// for which `expression` does not evaluate to values represented by `result`.
pub fn specialize_by_expression_result(
&mut self,
expression: &Expression,
result: Data,
) -> Result<(), Error> {
if let Expression::Var(var) = expression {
self.set_register(var, self.eval(expression).intersect(&result)?);
Ok(())
} else if let Expression::BinOp { op, lhs, rhs } = expression {
self.specialize_by_binop_expression_result(op, lhs, rhs, result)
} else {
match expression {
Expression::Var(_) => panic!(),
Expression::Const(input_bitvec) => {
if let Ok(result_bitvec) = result.try_to_bitvec() {
if *input_bitvec == result_bitvec {
Ok(())
} else {
Err(anyhow!("Unsatisfiable state"))
}
} else {
Ok(())
}
}
Expression::BinOp { .. } => {
panic!() // Already handled above
}
Expression::UnOp { op, arg } => {
use UnOpType::*;
match op {
IntNegate | BoolNegate | Int2Comp => {
let intermediate_result = result.un_op(*op);
self.specialize_by_expression_result(arg, intermediate_result)
}
_ => Ok(()),
}
}
Expression::Cast { op, size: _, arg } => match op {
CastOpType::IntZExt | CastOpType::IntSExt => {
let intermediate_result = result.subpiece(ByteSize::new(0), arg.bytesize());
self.specialize_by_expression_result(arg, intermediate_result)
}
_ => Ok(()),
},
Expression::Unknown {
description: _,
size: _,
} => Ok(()),
Expression::Subpiece {
low_byte,
size,
arg,
} => {
if *low_byte == ByteSize::new(0) {
if let Some(arg_value) = self.eval(expression).get_if_absolute_value() {
if arg_value.fits_into_size(*size) {
let intermediate_result =
result.cast(CastOpType::IntSExt, arg.bytesize());
return self
.specialize_by_expression_result(arg, intermediate_result);
}
}
}
Ok(())
}
}
}
}
/// Try to restrict the input variables of the given binary operation
/// so that it only evaluates to the given `result_bitvec`.
fn specialize_by_binop_expression_result(
&mut self,
op: &BinOpType,
lhs: &Expression,
rhs: &Expression,
result: Data,
) -> Result<(), Error> {
match op {
BinOpType::IntAdd => {
let intermediate_result = result.clone() - self.eval(lhs);
self.specialize_by_expression_result(rhs, intermediate_result)?;
let intermediate_result = result - self.eval(rhs);
self.specialize_by_expression_result(lhs, intermediate_result)?;
return Ok(());
}
BinOpType::IntSub => {
let intermediate_result: Data = self.eval(lhs) - result.clone();
self.specialize_by_expression_result(rhs, intermediate_result)?;
let intermediate_result = result + self.eval(rhs);
self.specialize_by_expression_result(lhs, intermediate_result)?;
return Ok(());
}
_ => (),
}
if let Ok(result_bitvec) = result.try_to_bitvec() {
match op {
BinOpType::IntXOr | BinOpType::BoolXOr => {
if let Ok(bitvec) = self.eval(lhs).try_to_bitvec() {
self.specialize_by_expression_result(
rhs,
(result_bitvec.clone() ^ &bitvec).into(),
)?;
}
if let Ok(bitvec) = self.eval(rhs).try_to_bitvec() {
self.specialize_by_expression_result(
lhs,
(result_bitvec ^ &bitvec).into(),
)?;
}
Ok(())
}
BinOpType::IntOr | BinOpType::BoolOr => {
if result_bitvec.is_zero() {
self.specialize_by_expression_result(lhs, result_bitvec.clone().into())?;
self.specialize_by_expression_result(rhs, result_bitvec.into())
} else if self
.eval(lhs)
.try_to_bitvec()
.map_or(false, |bitvec| bitvec.is_zero())
{
self.specialize_by_expression_result(rhs, result_bitvec.into())
} else if self
.eval(rhs)
.try_to_bitvec()
.map_or(false, |bitvec| bitvec.is_zero())
{
self.specialize_by_expression_result(lhs, result_bitvec.into())
} else {
Ok(())
}
}
BinOpType::BoolAnd => {
if !result_bitvec.is_zero() {
self.specialize_by_expression_result(lhs, result_bitvec.clone().into())?;
self.specialize_by_expression_result(rhs, result_bitvec.into())
} else if self
.eval(lhs)
.try_to_bitvec()
.map_or(false, |bitvec| !bitvec.is_zero())
{
self.specialize_by_expression_result(rhs, result_bitvec.into())
} else if self
.eval(rhs)
.try_to_bitvec()
.map_or(false, |bitvec| !bitvec.is_zero())
{
self.specialize_by_expression_result(lhs, result_bitvec.into())
} else {
Ok(())
}
}
BinOpType::IntEqual | BinOpType::IntNotEqual => {
match (op, !result_bitvec.is_zero()) {
(BinOpType::IntEqual, true) | (BinOpType::IntNotEqual, false) => {
// lhs == rhs
if let Ok(bitvec) = self.eval(lhs).try_to_bitvec() {
self.specialize_by_expression_result(rhs, bitvec.into())?;
}
if let Ok(bitvec) = self.eval(rhs).try_to_bitvec() {
self.specialize_by_expression_result(lhs, bitvec.into())?;
}
// Also specialize cases of pointer comparisons
self.specialize_pointer_comparison(&BinOpType::IntEqual, lhs, rhs)?;
Ok(())
}
(BinOpType::IntEqual, false) | (BinOpType::IntNotEqual, true) => {
// lhs != rhs
if let Ok(bitvec) = self.eval(lhs).try_to_bitvec() {
let new_result = self.eval(rhs).add_not_equal_bound(&bitvec)?;
self.specialize_by_expression_result(rhs, new_result)?;
}
if let Ok(bitvec) = self.eval(rhs).try_to_bitvec() {
let new_result = self.eval(lhs).add_not_equal_bound(&bitvec)?;
self.specialize_by_expression_result(lhs, new_result)?;
}
// Also specialize cases of pointer comparisons
self.specialize_pointer_comparison(&BinOpType::IntNotEqual, lhs, rhs)?;
Ok(())
}
_ => panic!(),
}
}
BinOpType::IntSLess
| BinOpType::IntLess
| BinOpType::IntLessEqual
| BinOpType::IntSLessEqual => {
use BinOpType::*;
let mut op = *op;
let (mut left_expr, mut right_expr) = (lhs, rhs);
if result_bitvec.is_zero() {
std::mem::swap(&mut left_expr, &mut right_expr);
op = match op {
IntSLess => IntSLessEqual,
IntSLessEqual => IntSLess,
IntLess => IntLessEqual,
IntLessEqual => IntLess,
_ => panic!(),
}
}
self.specialize_by_comparison_op(&op, left_expr, right_expr)
}
_ => {
let original_expression = Expression::BinOp {
lhs: Box::new(lhs.clone()),
op: *op,
rhs: Box::new(rhs.clone()),
};
if let Ok(interval) = self.eval(&original_expression).try_to_interval() {
if !interval.contains(&result_bitvec) {
Err(anyhow!("Unsatisfiable bound"))
} else {
Ok(())
}
} else {
Ok(())
}
}
}
} else {
Ok(())
}
}
/// If both `lhs` and `rhs` evaluate to pointers and `op` is a comparison operator that evaluates to `true`,
/// specialize the input pointers accordingly.
///
/// Note that the current implementation only specializes for `==` and `!=` operators
/// and only if the pointers point to the same unique memory object.
fn specialize_pointer_comparison(
&mut self,
op: &BinOpType,
lhs: &Expression,
rhs: &Expression,
) -> Result<(), Error> {
let (lhs_pointer, rhs_pointer) = (self.eval(lhs), self.eval(rhs));
match (
lhs_pointer.get_if_unique_target(),
rhs_pointer.get_if_unique_target(),
) {
(Some((lhs_id, lhs_offset)), Some((rhs_id, rhs_offset))) if lhs_id == rhs_id => {
if !(self.memory.is_unique_object(lhs_id)?) {
// Since the pointers may or may not point to different instances referenced by the same ID we cannot compare them.
return Ok(());
}
if *op == BinOpType::IntEqual {
let specialized_offset = lhs_offset.clone().intersect(rhs_offset)?;
let specialized_domain: Data =
Data::from_target(lhs_id.clone(), specialized_offset);
self.specialize_by_expression_result(lhs, specialized_domain.clone())?;
self.specialize_by_expression_result(rhs, specialized_domain)?;
} else if *op == BinOpType::IntNotEqual {
if let Ok(rhs_offset_bitvec) = rhs_offset.try_to_bitvec() {
let new_lhs_offset =
lhs_offset.clone().add_not_equal_bound(&rhs_offset_bitvec)?;
self.specialize_by_expression_result(
lhs,
Data::from_target(lhs_id.clone(), new_lhs_offset),
)?;
}
if let Ok(lhs_offset_bitvec) = lhs_offset.try_to_bitvec() {
let new_rhs_offset =
rhs_offset.clone().add_not_equal_bound(&lhs_offset_bitvec)?;
self.specialize_by_expression_result(
rhs,
Data::from_target(rhs_id.clone(), new_rhs_offset),
)?;
}
}
}
_ => (), // Other cases not handled, since it depends on the meaning of pointer IDs, which may change in the future.
}
Ok(())
}
/// Try to restrict the input variables of the given comparison operation
/// (signed and unsigned versions of `<` and `<=`)
/// so that the comparison evaluates to `true`.
fn specialize_by_comparison_op(
&mut self,
op: &BinOpType,
lhs: &Expression,
rhs: &Expression,
) -> Result<(), Error> {
use BinOpType::*;
if let Ok(mut lhs_bound) = self.eval(lhs).try_to_bitvec() {
match op {
IntSLess => {
if lhs_bound == Bitvector::signed_max_value(lhs_bound.width()) {
return Err(anyhow!("Unsatisfiable bound"));
}
lhs_bound += &Bitvector::one(lhs_bound.width());
let new_result = self.eval(rhs).add_signed_greater_equal_bound(&lhs_bound)?;
self.specialize_by_expression_result(rhs, new_result)?;
}
IntSLessEqual => {
let new_result = self.eval(rhs).add_signed_greater_equal_bound(&lhs_bound)?;
self.specialize_by_expression_result(rhs, new_result)?;
}
IntLess => {
if lhs_bound == Bitvector::unsigned_max_value(lhs_bound.width()) {
return Err(anyhow!("Unsatisfiable bound"));
}
lhs_bound += &Bitvector::one(lhs_bound.width());
let new_result = self
.eval(rhs)
.add_unsigned_greater_equal_bound(&lhs_bound)?;
self.specialize_by_expression_result(rhs, new_result)?;
}
IntLessEqual => {
let new_result = self
.eval(rhs)
.add_unsigned_greater_equal_bound(&lhs_bound)?;
self.specialize_by_expression_result(rhs, new_result)?;
}
_ => panic!(),
}
}
if let Ok(mut rhs_bound) = self.eval(rhs).try_to_bitvec() {
match op {
IntSLess => {
if rhs_bound == Bitvector::signed_min_value(rhs_bound.width()) {
return Err(anyhow!("Unsatisfiable bound"));
}
rhs_bound -= &Bitvector::one(rhs_bound.width());
let new_result = self.eval(lhs).add_signed_less_equal_bound(&rhs_bound)?;
self.specialize_by_expression_result(lhs, new_result)?;
}
IntSLessEqual => {
let new_result = self.eval(lhs).add_signed_less_equal_bound(&rhs_bound)?;
self.specialize_by_expression_result(lhs, new_result)?;
}
IntLess => {
if rhs_bound == Bitvector::zero(rhs_bound.width()) {
return Err(anyhow!("Unsatisfiable bound"));
}
rhs_bound -= &Bitvector::one(rhs_bound.width());
let new_result = self.eval(lhs).add_unsigned_less_equal_bound(&rhs_bound)?;
self.specialize_by_expression_result(lhs, new_result)?;
}
IntLessEqual => {
let new_result = self.eval(lhs).add_unsigned_less_equal_bound(&rhs_bound)?;
self.specialize_by_expression_result(lhs, new_result)?;
}
_ => panic!(),
}
}
Ok(())
}
}
impl AbstractDomain for State {
......
src/cwe_checker_lib/src/analysis/pointer_inference/state/value_specialization.rs 0 → 100644
//! Methods of [`State`] for specializing values through comparison operations.
use super::*;
impl State {
/// Try to restrict the input variables of `expression` on `self`
/// so that `expression` only evaluates to values represented by the given `result`.
///
/// If `expression` cannot evaluate to any value represented by `self`, return an error.
///
/// This function may restrict to upper bounds of possible values
/// if the restriction cannot be made exact,
/// i.e. after calling this function the state may still contain values
/// for which `expression` does not evaluate to values represented by `result`.
pub fn specialize_by_expression_result(
&mut self,
expression: &Expression,
result: Data,
) -> Result<(), Error> {
if let Expression::Var(var) = expression {
self.set_register(var, self.eval(expression).intersect(&result)?);
Ok(())
} else if let Expression::BinOp { op, lhs, rhs } = expression {
self.specialize_by_binop_expression_result(op, lhs, rhs, result)
} else {
match expression {
Expression::Var(_) => panic!(),
Expression::Const(input_bitvec) => {
if let Ok(result_bitvec) = result.try_to_bitvec() {
if *input_bitvec == result_bitvec {
Ok(())
} else {
Err(anyhow!("Unsatisfiable state"))
}
} else {
Ok(())
}
}
Expression::BinOp { .. } => {
panic!() // Already handled above
}
Expression::UnOp { op, arg } => {
use UnOpType::*;
match op {
IntNegate | BoolNegate | Int2Comp => {
let intermediate_result = result.un_op(*op);
self.specialize_by_expression_result(arg, intermediate_result)
}
_ => Ok(()),
}
}
Expression::Cast { op, size: _, arg } => match op {
CastOpType::IntZExt | CastOpType::IntSExt => {
let intermediate_result = result.subpiece(ByteSize::new(0), arg.bytesize());
self.specialize_by_expression_result(arg, intermediate_result)
}
_ => Ok(()),
},
Expression::Unknown {
description: _,
size: _,
} => Ok(()),
Expression::Subpiece {
low_byte,
size,
arg,
} => {
if *low_byte == ByteSize::new(0) {
if let Some(arg_value) = self.eval(expression).get_if_absolute_value() {
if arg_value.fits_into_size(*size) {
let intermediate_result =
result.cast(CastOpType::IntSExt, arg.bytesize());
return self
.specialize_by_expression_result(arg, intermediate_result);
}
}
}
Ok(())
}
}
}
}
/// Try to restrict the input variables of the given binary operation
/// so that it only evaluates to the given `result_bitvec`.
fn specialize_by_binop_expression_result(
&mut self,
op: &BinOpType,
lhs: &Expression,
rhs: &Expression,
result: Data,
) -> Result<(), Error> {
match op {
BinOpType::IntAdd => {
let intermediate_result = result.clone() - self.eval(lhs);
self.specialize_by_expression_result(rhs, intermediate_result)?;
let intermediate_result = result - self.eval(rhs);
self.specialize_by_expression_result(lhs, intermediate_result)?;
return Ok(());
}
BinOpType::IntSub => {
let intermediate_result: Data = self.eval(lhs) - result.clone();
self.specialize_by_expression_result(rhs, intermediate_result)?;
let intermediate_result = result + self.eval(rhs);
self.specialize_by_expression_result(lhs, intermediate_result)?;
return Ok(());
}
_ => (),
}
if let Ok(result_bitvec) = result.try_to_bitvec() {
match op {
BinOpType::IntXOr | BinOpType::BoolXOr => {
if let Ok(bitvec) = self.eval(lhs).try_to_bitvec() {
self.specialize_by_expression_result(
rhs,
(result_bitvec.clone() ^ &bitvec).into(),
)?;
}
if let Ok(bitvec) = self.eval(rhs).try_to_bitvec() {
self.specialize_by_expression_result(
lhs,
(result_bitvec ^ &bitvec).into(),
)?;
}
Ok(())
}
BinOpType::IntOr | BinOpType::BoolOr => {
if result_bitvec.is_zero() {
self.specialize_by_expression_result(lhs, result_bitvec.clone().into())?;
self.specialize_by_expression_result(rhs, result_bitvec.into())
} else if self
.eval(lhs)
.try_to_bitvec()
.map_or(false, |bitvec| bitvec.is_zero())
{
self.specialize_by_expression_result(rhs, result_bitvec.into())
} else if self
.eval(rhs)
.try_to_bitvec()
.map_or(false, |bitvec| bitvec.is_zero())
{
self.specialize_by_expression_result(lhs, result_bitvec.into())
} else {
Ok(())
}
}
BinOpType::BoolAnd => {
if !result_bitvec.is_zero() {
self.specialize_by_expression_result(lhs, result_bitvec.clone().into())?;
self.specialize_by_expression_result(rhs, result_bitvec.into())
} else if self
.eval(lhs)
.try_to_bitvec()
.map_or(false, |bitvec| !bitvec.is_zero())
{
self.specialize_by_expression_result(rhs, result_bitvec.into())
} else if self
.eval(rhs)
.try_to_bitvec()
.map_or(false, |bitvec| !bitvec.is_zero())
{
self.specialize_by_expression_result(lhs, result_bitvec.into())
} else {
Ok(())
}
}
BinOpType::IntEqual | BinOpType::IntNotEqual => {
match (op, !result_bitvec.is_zero()) {
(BinOpType::IntEqual, true) | (BinOpType::IntNotEqual, false) => {
// lhs == rhs
if let Ok(bitvec) = self.eval(lhs).try_to_bitvec() {
self.specialize_by_expression_result(rhs, bitvec.into())?;
}
if let Ok(bitvec) = self.eval(rhs).try_to_bitvec() {
self.specialize_by_expression_result(lhs, bitvec.into())?;
}
// Also specialize cases of pointer comparisons
self.specialize_pointer_comparison(&BinOpType::IntEqual, lhs, rhs)?;
Ok(())
}
(BinOpType::IntEqual, false) | (BinOpType::IntNotEqual, true) => {
// lhs != rhs
if let Ok(bitvec) = self.eval(lhs).try_to_bitvec() {
let new_result = self.eval(rhs).add_not_equal_bound(&bitvec)?;
self.specialize_by_expression_result(rhs, new_result)?;
}
if let Ok(bitvec) = self.eval(rhs).try_to_bitvec() {
let new_result = self.eval(lhs).add_not_equal_bound(&bitvec)?;
self.specialize_by_expression_result(lhs, new_result)?;
}
// Also specialize cases of pointer comparisons
self.specialize_pointer_comparison(&BinOpType::IntNotEqual, lhs, rhs)?;
Ok(())
}
_ => panic!(),
}
}
BinOpType::IntSLess
| BinOpType::IntLess
| BinOpType::IntLessEqual
| BinOpType::IntSLessEqual => {
use BinOpType::*;
let mut op = *op;
let (mut left_expr, mut right_expr) = (lhs, rhs);
if result_bitvec.is_zero() {
std::mem::swap(&mut left_expr, &mut right_expr);
op = match op {
IntSLess => IntSLessEqual,
IntSLessEqual => IntSLess,
IntLess => IntLessEqual,
IntLessEqual => IntLess,
_ => panic!(),
}
}
self.specialize_by_comparison_op(&op, left_expr, right_expr)
}
_ => {
let original_expression = Expression::BinOp {
lhs: Box::new(lhs.clone()),
op: *op,
rhs: Box::new(rhs.clone()),
};
if let Ok(interval) = self.eval(&original_expression).try_to_interval() {
if !interval.contains(&result_bitvec) {
Err(anyhow!("Unsatisfiable bound"))
} else {
Ok(())
}
} else {
Ok(())
}
}
}
} else {
Ok(())
}
}
/// If both `lhs` and `rhs` evaluate to pointers and `op` is a comparison operator that evaluates to `true`,
/// specialize the input pointers accordingly.
///
/// Note that the current implementation only specializes for `==` and `!=` operators
/// and only if the pointers point to the same unique memory object.
fn specialize_pointer_comparison(
&mut self,
op: &BinOpType,
lhs: &Expression,
rhs: &Expression,
) -> Result<(), Error> {
let (lhs_pointer, rhs_pointer) = (self.eval(lhs), self.eval(rhs));
match (
lhs_pointer.get_if_unique_target(),
rhs_pointer.get_if_unique_target(),
) {
(Some((lhs_id, lhs_offset)), Some((rhs_id, rhs_offset))) if lhs_id == rhs_id => {
if !(self.memory.is_unique_object(lhs_id)?) {
// Since the pointers may or may not point to different instances referenced by the same ID we cannot compare them.
return Ok(());
}
if *op == BinOpType::IntEqual {
let specialized_offset = lhs_offset.clone().intersect(rhs_offset)?;
let specialized_domain: Data =
Data::from_target(lhs_id.clone(), specialized_offset);
self.specialize_by_expression_result(lhs, specialized_domain.clone())?;
self.specialize_by_expression_result(rhs, specialized_domain)?;
} else if *op == BinOpType::IntNotEqual {
if let Ok(rhs_offset_bitvec) = rhs_offset.try_to_bitvec() {
let new_lhs_offset =
lhs_offset.clone().add_not_equal_bound(&rhs_offset_bitvec)?;
self.specialize_by_expression_result(
lhs,
Data::from_target(lhs_id.clone(), new_lhs_offset),
)?;
}
if let Ok(lhs_offset_bitvec) = lhs_offset.try_to_bitvec() {
let new_rhs_offset =
rhs_offset.clone().add_not_equal_bound(&lhs_offset_bitvec)?;
self.specialize_by_expression_result(
rhs,
Data::from_target(rhs_id.clone(), new_rhs_offset),
)?;
}
}
}
_ => (), // Other cases not handled, since it depends on the meaning of pointer IDs, which may change in the future.
}
Ok(())
}
/// Try to restrict the input variables of the given comparison operation
/// (signed and unsigned versions of `<` and `<=`)
/// so that the comparison evaluates to `true`.
fn specialize_by_comparison_op(
&mut self,
op: &BinOpType,
lhs: &Expression,
rhs: &Expression,
) -> Result<(), Error> {
use BinOpType::*;
if let Ok(mut lhs_bound) = self.eval(lhs).try_to_bitvec() {
match op {
IntSLess => {
if lhs_bound == Bitvector::signed_max_value(lhs_bound.width()) {
return Err(anyhow!("Unsatisfiable bound"));
}
lhs_bound += &Bitvector::one(lhs_bound.width());
let new_result = self.eval(rhs).add_signed_greater_equal_bound(&lhs_bound)?;
self.specialize_by_expression_result(rhs, new_result)?;
}
IntSLessEqual => {
let new_result = self.eval(rhs).add_signed_greater_equal_bound(&lhs_bound)?;
self.specialize_by_expression_result(rhs, new_result)?;
}
IntLess => {
if lhs_bound == Bitvector::unsigned_max_value(lhs_bound.width()) {
return Err(anyhow!("Unsatisfiable bound"));
}
lhs_bound += &Bitvector::one(lhs_bound.width());
let new_result = self
.eval(rhs)
.add_unsigned_greater_equal_bound(&lhs_bound)?;
self.specialize_by_expression_result(rhs, new_result)?;
}
IntLessEqual => {
let new_result = self
.eval(rhs)
.add_unsigned_greater_equal_bound(&lhs_bound)?;
self.specialize_by_expression_result(rhs, new_result)?;
}
_ => panic!(),
}
}
if let Ok(mut rhs_bound) = self.eval(rhs).try_to_bitvec() {
match op {
IntSLess => {
if rhs_bound == Bitvector::signed_min_value(rhs_bound.width()) {
return Err(anyhow!("Unsatisfiable bound"));
}
rhs_bound -= &Bitvector::one(rhs_bound.width());
let new_result = self.eval(lhs).add_signed_less_equal_bound(&rhs_bound)?;
self.specialize_by_expression_result(lhs, new_result)?;
}
IntSLessEqual => {
let new_result = self.eval(lhs).add_signed_less_equal_bound(&rhs_bound)?;
self.specialize_by_expression_result(lhs, new_result)?;
}
IntLess => {
if rhs_bound == Bitvector::zero(rhs_bound.width()) {
return Err(anyhow!("Unsatisfiable bound"));
}
rhs_bound -= &Bitvector::one(rhs_bound.width());
let new_result = self.eval(lhs).add_unsigned_less_equal_bound(&rhs_bound)?;
self.specialize_by_expression_result(lhs, new_result)?;
}
IntLessEqual => {
let new_result = self.eval(lhs).add_unsigned_less_equal_bound(&rhs_bound)?;
self.specialize_by_expression_result(lhs, new_result)?;
}
_ => panic!(),
}
}
Ok(())
}
}
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment