Unverified Commit 97b32356 by Enkelmann Committed by GitHub

Fix comparison of relative values with NULL (#415)

parent d135a25e
......@@ -75,11 +75,19 @@ impl<T: SpecializeByConditional + RegisterDomain> SpecializeByConditional for Da
}
}
/// Compute the intersetion of two DataDomains.
///
/// Note that this implementation is unsound for several reasons:
/// - For example, it assumes that two different relative values cannot intersect.
/// But that is not true if their offfsets are big enough
/// or if the relative values do in fact reference the same object despite having different identifiers.
/// - If intersecting relative values with absolute values we represent the result with the absolute values.
/// But depending on the use-case an approximation by the relative values could be more precise.
fn intersect(self, other: &Self) -> Result<Self, Error> {
let result = match (self.contains_top_values, other.contains_top_values) {
let mut result = match (self.contains_top_values, other.contains_top_values) {
// If only one input value contains top elements, then the other input is the best approximation for the intersection.
(true, false) => other.clone(),
(false, true) => self,
(false, true) => self.clone(),
// Else we can compute the intersection field-wise.
(true, true) | (false, false) => {
let relative_values =
......@@ -99,6 +107,19 @@ impl<T: SpecializeByConditional + RegisterDomain> SpecializeByConditional for Da
}
}
};
// If one domain contains relative values and the other absolute values,
// then we have to assume that the relative values could represent any of the absolute values.
if let (true, Some(absolute_val)) =
(!self.relative_values.is_empty(), &other.absolute_value)
{
result = result.merge(&absolute_val.clone().into());
}
if let (Some(absolute_val), true) =
(&self.absolute_value, !other.relative_values.is_empty())
{
result = result.merge(&absolute_val.clone().into());
}
if result.is_empty() {
Err(anyhow!("Domain is empty."))
} else {
......@@ -129,36 +150,49 @@ mod tests {
#[test]
fn intersect() {
// Element-wise intersection
let mut targets = BTreeMap::new();
targets.insert(new_id("Rax"), IntervalDomain::mock(1, 1));
targets.insert(new_id("Rbx"), IntervalDomain::mock(1, 10));
let mut data_left = DataDomain::mock_from_target_map(targets);
data_left.set_absolute_value(Some(IntervalDomain::mock(1, 10)));
let data_left = DataDomain::mock_from_target_map(targets);
let mut targets = BTreeMap::new();
targets.insert(new_id("Rax"), IntervalDomain::mock(3, 3));
targets.insert(new_id("Rbx"), IntervalDomain::mock(5, 15));
targets.insert(new_id("Rcx"), IntervalDomain::mock(1, 1));
let mut data_right = DataDomain::mock_from_target_map(targets);
data_right.set_absolute_value(Some(IntervalDomain::mock(10, 20)));
// Element-wise intersection
let data_right = DataDomain::mock_from_target_map(targets);
let intersection = data_left.intersect(&data_right).unwrap();
assert_eq!(intersection.relative_values.len(), 1);
assert_eq!(
*intersection.relative_values.get(&new_id("Rbx")).unwrap(),
IntervalDomain::mock(5, 10)
);
assert_eq!(intersection.absolute_value.is_none(), true);
assert_eq!(intersection.contains_top_values, false);
// Intersection when one side contains relative values and the other absolute values
let mut targets = BTreeMap::new();
targets.insert(new_id("Rax"), IntervalDomain::mock(1, 1));
targets.insert(new_id("Rbx"), IntervalDomain::mock(1, 10));
let data_left = DataDomain::mock_from_target_map(targets);
let data_right = DataDomain::from(IntervalDomain::mock(10, 20));
let intersection = data_left.clone().intersect(&data_right).unwrap();
assert_eq!(intersection.relative_values.len(), 0);
assert_eq!(
intersection.absolute_value,
Some(IntervalDomain::mock(10, 10))
Some(IntervalDomain::mock(10, 20))
);
assert_eq!(intersection.contains_top_values, false);
// Intersection where exactly one side contains top elements
let mut data_with_top = DataDomain::new_top(ByteSize::new(8));
data_with_top.set_absolute_value(Some(IntervalDomain::mock(15, 100)));
let intersection = data_right.clone().intersect(&data_with_top).unwrap();
assert_eq!(intersection, data_right);
let data_with_top = DataDomain::new_top(ByteSize::new(8));
let intersection = data_left.clone().intersect(&data_with_top).unwrap();
assert_eq!(intersection, data_left);
// Empty intersection
let data_absolute_val = IntervalDomain::mock(100, 100).into();
assert!(data_right.intersect(&data_absolute_val).is_err());
// NOTE: The checked behavior may actually be unsound depending on the use-case of the domain:
// Two different relative values may be allowed to represent the same object/number.
let data_left = DataDomain::from_target(new_id("RAX"), IntervalDomain::mock(0, 5));
let data_right = DataDomain::from_target(new_id("RBX"), IntervalDomain::mock(0, 5));
assert!(data_left.intersect(&data_right).is_err());
}
}
......@@ -5,25 +5,25 @@ use crate::intermediate_representation::*;
use crate::prelude::*;
mod bitvector;
pub use bitvector::*;
pub use bitvector::BitvectorDomain;
mod identifier;
pub use identifier::*;
mod data;
pub use data::*;
pub use data::DataDomain;
mod mem_region;
pub use mem_region::*;
pub use mem_region::MemRegion;
mod interval;
pub use interval::*;
pub use interval::{Interval, IntervalDomain};
mod bricks;
pub use bricks::*;
pub use bricks::{BrickDomain, BricksDomain};
mod character_inclusion;
pub use character_inclusion::*;
pub use character_inclusion::{CharacterInclusionDomain, CharacterSet};
mod strings;
pub use strings::*;
......
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