Use IntervalDomain in Pointer Inference analysis (#158)

src/cwe_checker_lib/src/abstract_domain/bitvector.rs

-use super::{AbstractDomain, HasTop, RegisterDomain, SizedDomain};
+use super::Interval;
+use super::{AbstractDomain, HasTop, RegisterDomain, SizedDomain, TryToBitvec, TryToInterval};
 use crate::intermediate_representation::*;
 use crate::prelude::*;
 
@@ -141,12 +142,22 @@ impl std::convert::From<Bitvector> for BitvectorDomain {
     }
 }
 
-impl std::convert::TryFrom<&BitvectorDomain> for Bitvector {
-    type Error = ();
-    fn try_from(bitvec_domain: &BitvectorDomain) -> Result<Bitvector, ()> {
-        match bitvec_domain {
-            BitvectorDomain::Value(bitvec) => Ok(bitvec.clone()),
-            BitvectorDomain::Top(_) => Err(()),
+impl TryToBitvec for BitvectorDomain {
+    /// If the domain represents an absoulute value, return it.
+    fn try_to_bitvec(&self) -> Result<Bitvector, Error> {
+        match self {
+            BitvectorDomain::Value(val) => Ok(val.clone()),
+            BitvectorDomain::Top(_) => Err(anyhow!("Value is Top")),
+        }
+    }
+}
+
+impl TryToInterval for BitvectorDomain {
+    /// If the domain represents an absolute value, return it as an interval of length one.
+    fn try_to_interval(&self) -> Result<Interval, Error> {
+        match self {
+            BitvectorDomain::Value(val) => Ok(Interval::new(val.clone(), val.clone())),
+            BitvectorDomain::Top(_) => Err(anyhow!("Value is Top")),
         }
     }
 }

src/cwe_checker_lib/src/abstract_domain/data.rs

 use super::{
-    AbstractDomain, AbstractIdentifier, HasTop, PointerDomain, RegisterDomain, SizedDomain,
+    AbstractDomain, AbstractIdentifier, HasTop, Interval, PointerDomain, RegisterDomain,
+    SizedDomain, TryToBitvec, TryToInterval,
 };
 use crate::intermediate_representation::*;
 use crate::prelude::*;
@@ -221,6 +222,28 @@ impl<T: RegisterDomain + From<Bitvector>> From<Bitvector> for DataDomain<T> {
     }
 }
 
+impl<T: RegisterDomain + TryToBitvec> TryToBitvec for DataDomain<T> {
+    /// If the domain represents a single, absolute value, return it.
+    fn try_to_bitvec(&self) -> Result<Bitvector, Error> {
+        match self {
+            DataDomain::Value(value) => value.try_to_bitvec(),
+            DataDomain::Pointer(_) => Err(anyhow!("Value is a pointer.")),
+            DataDomain::Top(_) => Err(anyhow!("Value is Top")),
+        }
+    }
+}
+
+impl<T: RegisterDomain + TryToInterval> TryToInterval for DataDomain<T> {
+    /// If the domain represents (or can be widened to) an interval of absolute values, return the interval.
+    fn try_to_interval(&self) -> Result<Interval, Error> {
+        match self {
+            DataDomain::Value(value) => value.try_to_interval(),
+            DataDomain::Pointer(_) => Err(anyhow!("Value is a pointer.")),
+            DataDomain::Top(_) => Err(anyhow!("Value is Top")),
+        }
+    }
+}
+
 impl<T: RegisterDomain + Display> DataDomain<T> {
     /// Get a more compact json-representation of the data domain.
     /// Intended for pretty printing, not useable for serialization/deserialization.

src/cwe_checker_lib/src/abstract_domain/interval.rs

@@ -4,9 +4,10 @@ use crate::intermediate_representation::*;
 use crate::prelude::*;
 
 use super::{AbstractDomain, HasTop, RegisterDomain, SizedDomain};
+use super::{TryToBitvec, TryToInterval};
 
 mod simple_interval;
-use simple_interval::*;
+pub use simple_interval::*;
 
 mod bin_ops;
 
@@ -18,7 +19,7 @@ mod bin_ops;
 /// The domain also contains widening hints to faciliate fast and exact widening for simple loop counter variables.
 /// See the [`IntervalDomain::signed_merge_and_widen`] method for details on the widening strategy.
 #[derive(Serialize, Deserialize, Debug, PartialEq, Eq, Hash, Clone)]
-struct IntervalDomain {
+pub struct IntervalDomain {
     /// The underlying interval.
     interval: Interval,
     /// A lower bound for widening operations.
@@ -149,15 +150,6 @@ impl IntervalDomain {
         }
     }
 
-    /// If the interval contains exactly one value, return the value.
-    pub fn try_to_bitvec(&self) -> Result<Bitvector, ()> {
-        if self.interval.start == self.interval.end {
-            Ok(self.interval.start.clone())
-        } else {
-            Err(())
-        }
-    }
-
     /// Zero-extend the values in the interval to the given width.
     pub fn zero_extend(self, width: ByteSize) -> IntervalDomain {
         let lower_bound = match self.widening_lower_bound {
@@ -410,6 +402,30 @@ impl RegisterDomain for IntervalDomain {
     }
 }
 
+impl std::ops::Add for IntervalDomain {
+    type Output = IntervalDomain;
+
+    fn add(self, rhs: Self) -> Self {
+        self.bin_op(BinOpType::IntAdd, &rhs)
+    }
+}
+
+impl std::ops::Sub for IntervalDomain {
+    type Output = IntervalDomain;
+
+    fn sub(self, rhs: Self) -> Self {
+        self.bin_op(BinOpType::IntSub, &rhs)
+    }
+}
+
+impl std::ops::Neg for IntervalDomain {
+    type Output = IntervalDomain;
+
+    fn neg(self) -> Self {
+        self.un_op(UnOpType::Int2Comp)
+    }
+}
+
 impl From<Bitvector> for IntervalDomain {
     /// Create an interval containing only `bitvec`.
     fn from(bitvec: Bitvector) -> Self {
@@ -421,6 +437,28 @@ impl From<Bitvector> for IntervalDomain {
     }
 }
 
+impl TryToBitvec for IntervalDomain {
+    /// If the domain represents an interval of length one, return the contained value.
+    fn try_to_bitvec(&self) -> Result<Bitvector, Error> {
+        if self.interval.start == self.interval.end {
+            Ok(self.interval.start.clone())
+        } else {
+            Err(anyhow!("More than one value in the interval."))
+        }
+    }
+}
+
+impl TryToInterval for IntervalDomain {
+    /// If the domain represents a bounded (i.e. not `Top`) interval, return it.
+    fn try_to_interval(&self) -> Result<Interval, Error> {
+        if self.is_top() {
+            Err(anyhow!("Value is Top"))
+        } else {
+            Ok(self.interval.clone())
+        }
+    }
+}
+
 impl Display for IntervalDomain {
     fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
         if self.is_top() {

src/cwe_checker_lib/src/abstract_domain/mem_region.rs

@@ -109,6 +109,16 @@ impl<T: AbstractDomain + SizedDomain + HasTop + std::fmt::Debug> MemRegionData<T
         }
     }
 
+    /// Clear all values that might be overwritten if one writes a value with byte size `value_size`
+    /// to an offset contained in the interval from `start` to `end` (both bounds included in the interval).
+    ///
+    /// This represents the effect of writing an arbitrary value (with known byte size)
+    /// to an arbitrary offset contained in the interval.
+    pub fn clear_offset_interval(&mut self, start: i64, end: i64, value_size: ByteSize) {
+        let size = end - start + (u64::from(value_size) as i64);
+        self.clear_interval(start, size);
+    }
+
     /// Add a value to the memory region.
     pub fn add(&mut self, value: T, position: Bitvector) {
         assert_eq!(ByteSize::from(position.width()), self.address_bytesize);

src/cwe_checker_lib/src/abstract_domain/mod.rs

@@ -2,6 +2,7 @@
 //! as well as several abstract domain types implementing these traits.
 
 use crate::intermediate_representation::*;
+use crate::prelude::*;
 
 mod bitvector;
 pub use bitvector::*;
@@ -91,3 +92,34 @@ pub trait RegisterDomain: AbstractDomain + SizedDomain + HasTop {
         }
     }
 }
+
+/// A conversion trait for abstract domains that can represent register values.
+pub trait TryToBitvec {
+    /// If `self` represents a single absolute value, return it.
+    /// In all other cases return an error.
+    fn try_to_bitvec(&self) -> Result<Bitvector, Error>;
+
+    /// If `self` represents a single absolute value, try to convert it to a signed integer and return it.
+    /// Else return an error.
+    /// Note that the conversion loses information about the bytesize of the value.
+    fn try_to_offset(&self) -> Result<i64, Error> {
+        Ok(self.try_to_bitvec()?.try_to_i64()?)
+    }
+}
+
+/// A conversion trait for abstract domains that can represent register values.
+pub trait TryToInterval {
+    /// If `self` represents an interval of absolute values (or can be widened to represent such an interval)
+    /// then return it if the interval is bounded.
+    /// For unbounded (i.e. `Top`) intervals or if the abstract value does not represent absolute values return an error.
+    fn try_to_interval(&self) -> Result<Interval, Error>;
+
+    /// If `self` represents an interval of absolute values (or can be widened to represent such an interval)
+    /// then return it as an interval of signed integers if the interval is bounded.
+    /// Else return an error.
+    /// Note that the conversion loses information about the bytesize of the values contained in the interval.
+    fn try_to_offset_interval(&self) -> Result<(i64, i64), Error> {
+        let interval = self.try_to_interval()?;
+        Ok((interval.start.try_to_i64()?, interval.end.try_to_i64()?))
+    }
+}

src/cwe_checker_lib/src/analysis/pointer_inference/context/mod.rs

@@ -7,6 +7,7 @@ use crate::{abstract_domain::*, utils::binary::RuntimeMemoryImage};
 use std::collections::{BTreeMap, BTreeSet};
 
 use super::state::State;
+use super::ValueDomain;
 use super::{Config, Data, VERSION};
 
 // contains trait implementations for the `Context` struct,
@@ -380,7 +381,7 @@ impl<'a> Context<'a> {
     }
 
     /// Get the offset of the current stack pointer to the base of the current stack frame.
-    fn get_current_stack_offset(&self, state: &State) -> BitvectorDomain {
+    fn get_current_stack_offset(&self, state: &State) -> ValueDomain {
         if let Ok(Data::Pointer(ref stack_pointer)) =
             state.get_register(&self.project.stack_pointer_register)
         {
@@ -388,16 +389,11 @@ impl<'a> Context<'a> {
                 let (stack_id, stack_offset_domain) =
                     stack_pointer.targets().iter().next().unwrap();
                 if *stack_id == state.stack_id {
-                    stack_offset_domain.clone()
-                } else {
-                    BitvectorDomain::new_top(stack_pointer.bytesize())
+                    return stack_offset_domain.clone();
                 }
-            } else {
-                BitvectorDomain::new_top(self.project.stack_pointer_register.size)
             }
-        } else {
-            BitvectorDomain::new_top(self.project.stack_pointer_register.size)
         }
+        ValueDomain::new_top(self.project.stack_pointer_register.size)
     }
 }
 

src/cwe_checker_lib/src/analysis/pointer_inference/context/tests.rs

 use super::*;
 use std::collections::HashSet;
 
-fn bv(value: i64) -> BitvectorDomain {
-    BitvectorDomain::Value(Bitvector::from_i64(value))
+fn bv(value: i64) -> ValueDomain {
+    ValueDomain::from(Bitvector::from_i64(value))
 }
 
 fn new_id(time: &str, reg_name: &str) -> AbstractIdentifier {

src/cwe_checker_lib/src/analysis/pointer_inference/mod.rs

@@ -21,7 +21,7 @@ use crate::intermediate_representation::*;
 use crate::prelude::*;
 use crate::utils::log::*;
 use crate::{
-    abstract_domain::{BitvectorDomain, DataDomain},
+    abstract_domain::{DataDomain, IntervalDomain},
     utils::binary::RuntimeMemoryImage,
 };
 use petgraph::graph::NodeIndex;
@@ -47,8 +47,11 @@ pub static CWE_MODULE: crate::CweModule = crate::CweModule {
     run: extract_pi_analysis_results,
 };
 
+/// The abstract domain to use for absolute values.
+pub type ValueDomain = IntervalDomain;
+
 /// The abstract domain type for representing register values.
-pub type Data = DataDomain<BitvectorDomain>;
+pub type Data = DataDomain<ValueDomain>;
 
 /// Configurable parameters for the analysis.
 #[derive(Serialize, Deserialize, Debug, PartialEq, Eq, Hash, Clone)]

src/cwe_checker_lib/src/analysis/pointer_inference/object.rs

 //! This module contains the definition of the abstract memory object type.
 
-use super::Data;
+use super::{Data, ValueDomain};
 use crate::abstract_domain::*;
 use crate::prelude::*;
 use derive_more::Deref;
@@ -72,20 +72,23 @@ impl AbstractObjectInfo {
     ///
     /// If the abstract object is not unique (i.e. may represent more than one actual object),
     /// merge the old value at the given offset with the new value.
-    pub fn set_value(&mut self, value: Data, offset: &BitvectorDomain) -> Result<(), Error> {
+    pub fn set_value(&mut self, value: Data, offset: &ValueDomain) -> Result<(), Error> {
         if let Data::Pointer(ref pointer) = value {
             self.pointer_targets.extend(pointer.ids().cloned());
         };
-        if let BitvectorDomain::Value(ref concrete_offset) = offset {
+        if let Ok(concrete_offset) = offset.try_to_bitvec() {
             if self.is_unique {
-                self.memory.add(value, concrete_offset.clone());
+                self.memory.add(value, concrete_offset);
             } else {
                 let merged_value = self
                     .memory
                     .get(concrete_offset.clone(), value.bytesize())
                     .merge(&value);
-                self.memory.add(merged_value, concrete_offset.clone());
+                self.memory.add(merged_value, concrete_offset);
             };
+        } else if let Ok((start, end)) = offset.try_to_offset_interval() {
+            self.memory
+                .clear_offset_interval(start, end, value.bytesize());
         } else {
             self.memory = MemRegion::new(self.memory.get_address_bytesize());
         }
@@ -93,16 +96,19 @@ impl AbstractObjectInfo {
     }
 
     /// Merge `value` at position `offset` with the value currently saved at that position.
-    pub fn merge_value(&mut self, value: Data, offset: &BitvectorDomain) {
+    pub fn merge_value(&mut self, value: Data, offset: &ValueDomain) {
         if let Data::Pointer(ref pointer) = value {
             self.pointer_targets.extend(pointer.ids().cloned());
         };
-        if let BitvectorDomain::Value(ref concrete_offset) = offset {
+        if let Ok(concrete_offset) = offset.try_to_bitvec() {
             let merged_value = self
                 .memory
                 .get(concrete_offset.clone(), value.bytesize())
                 .merge(&value);
-            self.memory.add(merged_value, concrete_offset.clone());
+            self.memory.add(merged_value, concrete_offset);
+        } else if let Ok((start, end)) = offset.try_to_offset_interval() {
+            self.memory
+                .clear_offset_interval(start, end, value.bytesize());
         } else {
             self.memory = MemRegion::new(self.memory.get_address_bytesize());
         }
@@ -131,7 +137,7 @@ impl AbstractObjectInfo {
         &mut self,
         old_id: &AbstractIdentifier,
         new_id: &AbstractIdentifier,
-        offset_adjustment: &BitvectorDomain,
+        offset_adjustment: &ValueDomain,
     ) {
         for elem in self.memory.values_mut() {
             elem.replace_abstract_id(old_id, new_id, offset_adjustment);
@@ -323,8 +329,8 @@ mod tests {
         Data::Value(bv(number))
     }
 
-    fn bv(number: i64) -> BitvectorDomain {
-        BitvectorDomain::Value(Bitvector::from_i64(number))
+    fn bv(number: i64) -> ValueDomain {
+        ValueDomain::from(Bitvector::from_i64(number))
     }
 
     fn new_id(tid: &str, reg_name: &str) -> AbstractIdentifier {
@@ -353,10 +359,10 @@ mod tests {
             object.get_value(Bitvector::from_i64(-15), ByteSize::new(8)),
             Data::Top(ByteSize::new(8))
         );
-        object.merge_value(new_data(5), &bv(-12));
+        object.merge_value(new_data(23), &bv(-12));
         assert_eq!(
             object.get_value(Bitvector::from_i64(-12), ByteSize::new(8)),
-            Data::Value(BitvectorDomain::new_top(ByteSize::new(8)))
+            Data::Value(ValueDomain::new_top(ByteSize::new(8)))
         );
 
         let mut other_object = new_abstract_object();

src/cwe_checker_lib/src/analysis/pointer_inference/object_list.rs

 use super::object::*;
-use super::Data;
+use super::{Data, ValueDomain};
 use crate::abstract_domain::*;
 use crate::prelude::*;
 use serde::{Deserialize, Serialize};
@@ -14,11 +14,11 @@ use std::collections::{BTreeMap, BTreeSet};
 pub struct AbstractObjectList {
     /// The abstract objects.
     ///
-    /// Each abstract object comes with an offset given as a [`BitvectorDomain`].
+    /// Each abstract object comes with an offset given as a [`ValueDomain`].
     /// This offset determines where the zero offset corresponding to the abstract identifier inside the object is.
     /// Note that this offset may be a `Top` element
     /// if the exact offset corresponding to the identifier is unknown.
-    objects: BTreeMap<AbstractIdentifier, (AbstractObject, BitvectorDomain)>,
+    objects: BTreeMap<AbstractIdentifier, (AbstractObject, ValueDomain)>,
 }
 
 impl AbstractObjectList {
@@ -81,7 +81,7 @@ impl AbstractObjectList {
                 for (id, offset_pointer_domain) in pointer.targets() {
                     let (object, offset_identifier) = self.objects.get(id).unwrap();
                     let offset = offset_pointer_domain.clone() + offset_identifier.clone();
-                    if let BitvectorDomain::Value(concrete_offset) = offset {
+                    if let Ok(concrete_offset) = offset.try_to_bitvec() {
                         let value = object.get_value(concrete_offset, size);
                         merged_value = match merged_value {
                             Some(accum) => Some(accum.merge(&value)),
@@ -103,7 +103,7 @@ impl AbstractObjectList {
     /// we merge-write the value to all targets.
     pub fn set_value(
         &mut self,
-        pointer: PointerDomain<BitvectorDomain>,
+        pointer: PointerDomain<ValueDomain>,
         value: Data,
     ) -> Result<(), Error> {
         let targets = pointer.targets();
@@ -136,7 +136,7 @@ impl AbstractObjectList {
         &mut self,
         old_id: &AbstractIdentifier,
         new_id: &AbstractIdentifier,
-        offset_adjustment: &BitvectorDomain,
+        offset_adjustment: &ValueDomain,
     ) {
         let negative_offset = -offset_adjustment.clone();
         for (object, _) in self.objects.values_mut() {
@@ -160,7 +160,7 @@ impl AbstractObjectList {
     pub fn add_abstract_object(
         &mut self,
         object_id: AbstractIdentifier,
-        initial_offset: BitvectorDomain,
+        initial_offset: ValueDomain,
         type_: ObjectType,
         address_bytesize: ByteSize,
     ) {
@@ -225,7 +225,7 @@ impl AbstractObjectList {
     /// Returns either a non-empty list of detected errors (like possible double frees) or `OK(())` if no errors were found.
     pub fn mark_mem_object_as_freed(
         &mut self,
-        object_pointer: &PointerDomain<BitvectorDomain>,
+        object_pointer: &PointerDomain<ValueDomain>,
     ) -> Result<(), Vec<(AbstractIdentifier, Error)>> {
         let ids: Vec<AbstractIdentifier> = object_pointer.ids().cloned().collect();
         let mut possible_double_free_ids = Vec::new();
@@ -358,8 +358,8 @@ impl AbstractObjectList {
 mod tests {
     use super::*;
 
-    fn bv(value: i64) -> BitvectorDomain {
-        BitvectorDomain::Value(Bitvector::from_i64(value))
+    fn bv(value: i64) -> ValueDomain {
+        ValueDomain::from(Bitvector::from_i64(value))
     }
 
     fn new_id(name: &str) -> AbstractIdentifier {
@@ -442,7 +442,7 @@ mod tests {
             merged
                 .get_value(&Data::Pointer(pointer.clone()), ByteSize::new(8))
                 .unwrap(),
-            Data::Value(BitvectorDomain::new_top(ByteSize::new(8)))
+            Data::Value(ValueDomain::new_top(ByteSize::new(8)))
         );
         assert_eq!(
             merged

src/cwe_checker_lib/src/analysis/pointer_inference/state/access_handling.rs

@@ -86,14 +86,25 @@ impl State {
                     self.memory.set_value(pointer, value.clone())?;
                     Ok(())
                 }
-                Data::Value(BitvectorDomain::Value(address_to_global_data)) => {
-                    match global_memory.is_address_writeable(&address_to_global_data) {
-                        Ok(true) => Ok(()),
-                        Ok(false) => Err(anyhow!("Write to read-only global data")),
-                        Err(err) => Err(err),
+                Data::Value(absolute_address) => {
+                    if let Ok(address_to_global_data) = absolute_address.try_to_bitvec() {
+                        match global_memory.is_address_writeable(&address_to_global_data) {
+                            Ok(true) => Ok(()),
+                            Ok(false) => Err(anyhow!("Write to read-only global data")),
+                            Err(err) => Err(err),
+                        }
+                    } else if let Ok((start, end)) = absolute_address.try_to_offset_interval() {
+                        match global_memory.is_interval_writeable(start as u64, end as u64) {
+                            Ok(true) => Ok(()),
+                            Ok(false) => Err(anyhow!("Write to read-only global data")),
+                            Err(err) => Err(err),
+                        }
+                    } else {
+                        // We assume inexactness of the algorithm instead of a possible CWE here.
+                        Ok(())
                     }
                 }
-                Data::Value(BitvectorDomain::Top(_)) | Data::Top(_) => Ok(()),
+                Data::Top(_) => Ok(()),
             }
         }
     }
@@ -142,15 +153,26 @@ impl State {
     ) -> Result<Data, Error> {
         let address = self.adjust_pointer_for_read(&self.eval(address)?);
         match address {
-            Data::Value(BitvectorDomain::Value(address_bitvector)) => {
-                let loaded_value = global_memory.read(&address_bitvector, size)?;
-                if loaded_value.is_top() {
-                    Ok(Data::Top(loaded_value.bytesize()))
+            Data::Value(global_address) => {
+                if let Ok(address_bitvector) = global_address.try_to_bitvec() {
+                    if let Some(loaded_value) = global_memory.read(&address_bitvector, size)? {
+                        Ok(Data::Value(loaded_value.into()))
+                    } else {
+                        Ok(Data::Top(size))
+                    }
+                } else if let Ok((start, end)) = global_address.try_to_offset_interval() {
+                    if global_memory
+                        .is_interval_readable(start as u64, end as u64 + u64::from(size))?
+                    {
+                        Ok(Data::new_top(size))
+                    } else {
+                        Err(anyhow!("Target address is not readable."))
+                    }
                 } else {
-                    Ok(Data::Value(loaded_value))
+                    Ok(Data::new_top(size))
                 }
             }
-            Data::Value(BitvectorDomain::Top(_)) | Data::Top(_) => Ok(Data::new_top(size)),
+            Data::Top(_) => Ok(Data::new_top(size)),
             Data::Pointer(_) => Ok(self.memory.get_value(&address, size)?),
         }
     }
@@ -181,26 +203,24 @@ impl State {
             let mut new_targets = BTreeMap::new();
             for (id, offset) in pointer.targets() {
                 if *id == self.stack_id {
-                    match offset {
-                        BitvectorDomain::Value(offset_val) => {
-                            if offset_val.try_to_i64().unwrap() >= 0
-                                && !self.caller_stack_ids.is_empty()
-                            {
-                                for caller_id in self.caller_stack_ids.iter() {
-                                    new_targets.insert(caller_id.clone(), offset.clone());
-                                }
-                            // Note that the id of the current stack frame was *not* added.
-                            } else {
-                                new_targets.insert(id.clone(), offset.clone());
-                            }
-                        }
-                        BitvectorDomain::Top(_bytesize) => {
+                    if let Ok((interval_start, interval_end)) = offset.try_to_offset_interval() {
+                        if interval_start >= 0
+                            && interval_end >= 0
+                            && !self.caller_stack_ids.is_empty()
+                        {
                             for caller_id in self.caller_stack_ids.iter() {
                                 new_targets.insert(caller_id.clone(), offset.clone());
                             }
-                            // Note that we also add the id of the current stack frame
+                        // Note that the id of the current stack frame was *not* added.
+                        } else {
                             new_targets.insert(id.clone(), offset.clone());
                         }
+                    } else {
+                        for caller_id in self.caller_stack_ids.iter() {
+                            new_targets.insert(caller_id.clone(), offset.clone());
+                        }
+                        // Note that we also add the id of the current stack frame
+                        new_targets.insert(id.clone(), offset.clone());
                     }
                 } else {
                     new_targets.insert(id.clone(), offset.clone());
@@ -275,15 +295,15 @@ impl State {
     /// i.e. it is an access to the caller stack, return the offset.
     ///
     /// In all other cases, including the case that the address has more than one target, return `None`.
-    fn unwrap_offset_if_caller_stack_address(&self, address: &Data) -> Option<BitvectorDomain> {
+    fn unwrap_offset_if_caller_stack_address(&self, address: &Data) -> Option<ValueDomain> {
         if self.caller_stack_ids.is_empty() {
             return None;
         }
         if let Data::Pointer(pointer) = address {
             match (pointer.targets().len(), pointer.targets().iter().next()) {
                 (1, Some((id, offset))) if self.stack_id == *id => {
-                    if let BitvectorDomain::Value(offset_val) = offset {
-                        if offset_val.try_to_i64().unwrap() >= 0 {
+                    if let Ok((interval_start, _interval_end)) = offset.try_to_offset_interval() {
+                        if interval_start >= 0 {
                             return Some(offset.clone());
                         }
                     }

src/cwe_checker_lib/src/analysis/pointer_inference/state/mod.rs

 use super::object_list::AbstractObjectList;
-use super::Data;
+use super::{Data, ValueDomain};
 use crate::abstract_domain::*;
 use crate::intermediate_representation::*;
 use crate::prelude::*;
@@ -124,7 +124,7 @@ impl State {
         &mut self,
         old_id: &AbstractIdentifier,
         new_id: &AbstractIdentifier,
-        offset_adjustment: &BitvectorDomain,
+        offset_adjustment: &ValueDomain,
     ) {
         for register_data in self.register.values_mut() {
             register_data.replace_abstract_id(old_id, new_id, &(-offset_adjustment.clone()));
@@ -226,7 +226,7 @@ impl State {
         &mut self,
         callee_id: &AbstractIdentifier,
         caller_id: &AbstractIdentifier,
-        offset_adjustment: &BitvectorDomain,
+        offset_adjustment: &ValueDomain,
     ) {
         self.memory.remove_object(callee_id);
         self.replace_abstract_id(callee_id, caller_id, offset_adjustment);
@@ -239,7 +239,7 @@ impl State {
     /// an error with the list of possibly already freed objects is returned.
     pub fn mark_mem_object_as_freed(
         &mut self,
-        object_pointer: &PointerDomain<BitvectorDomain>,
+        object_pointer: &PointerDomain<ValueDomain>,
     ) -> Result<(), Vec<(AbstractIdentifier, Error)>> {
         self.memory.mark_mem_object_as_freed(object_pointer)
     }

src/cwe_checker_lib/src/analysis/pointer_inference/state/tests.rs

 use super::*;
 use crate::utils::binary::RuntimeMemoryImage;
 
-fn bv(value: i64) -> BitvectorDomain {
-    BitvectorDomain::Value(Bitvector::from_i64(value))
+fn bv(value: i64) -> ValueDomain {
+    ValueDomain::from(Bitvector::from_i64(value))
 }
 
 fn new_id(time: &str, register: &str) -> AbstractIdentifier {
@@ -418,7 +418,7 @@ fn reachable_ids_under_and_overapproximation() {
     );
 
     let _ = state.store_value(
-        &PointerDomain::new(stack_id.clone(), BitvectorDomain::new_top(ByteSize::new(8))).into(),
+        &PointerDomain::new(stack_id.clone(), ValueDomain::new_top(ByteSize::new(8))).into(),
         &Data::Value(Bitvector::from_i64(42).into()),
         &global_memory,
     );

src/cwe_checker_lib/src/checkers/cwe_467.rs

@@ -20,7 +20,7 @@
 //! - If the incorrect size value is generated before the basic block that contains
 //! the call, the check will not be able to find it.
 
-use crate::abstract_domain::{BitvectorDomain, DataDomain};
+use crate::abstract_domain::TryToBitvec;
 use crate::analysis::pointer_inference::State;
 use crate::intermediate_representation::*;
 use crate::prelude::*;
@@ -79,11 +79,13 @@ fn check_for_pointer_sized_arg(
     let pointer_size = project.stack_pointer_register.size;
     let state = compute_block_end_state(project, global_memory, block);
     for parameter in symbol.parameters.iter() {
-        if let Ok(DataDomain::Value(BitvectorDomain::Value(param_value))) =
+        if let Ok(param) =
             state.eval_parameter_arg(parameter, &project.stack_pointer_register, global_memory)
         {
-            if Ok(u64::from(pointer_size)) == param_value.try_to_u64() {
-                return true;
+            if let Ok(param_value) = param.try_to_bitvec() {
+                if Ok(u64::from(pointer_size)) == param_value.try_to_u64() {
+                    return true;
+                }
             }
         }
     }

src/cwe_checker_lib/src/checkers/cwe_476/state.rs

 use crate::abstract_domain::{
-    AbstractDomain, AbstractIdentifier, BitvectorDomain, MemRegion, RegisterDomain, SizedDomain,
+    AbstractDomain, AbstractIdentifier, MemRegion, RegisterDomain, SizedDomain, TryToBitvec,
 };
 use crate::analysis::pointer_inference::Data;
 use crate::analysis::pointer_inference::State as PointerInferenceState;
@@ -153,8 +153,8 @@ impl State {
         let mut taint = Taint::Top(size);
         if let Data::Pointer(pointer) = address {
             for (mem_id, offset) in pointer.targets().iter() {
-                if let (Some(mem_region), BitvectorDomain::Value(position)) =
-                    (self.memory_taint.get(mem_id), offset)
+                if let (Some(mem_region), Ok(position)) =
+                    (self.memory_taint.get(mem_id), offset.try_to_bitvec())
                 {
                     taint = taint.merge(&mem_region.get(position.clone(), size));
                 }
@@ -172,7 +172,7 @@ impl State {
         if let Data::Pointer(pointer) = address {
             if pointer.targets().len() == 1 {
                 for (mem_id, offset) in pointer.targets().iter() {
-                    if let BitvectorDomain::Value(position) = offset {
+                    if let Ok(position) = offset.try_to_bitvec() {
                         if let Some(mem_region) = self.memory_taint.get_mut(mem_id) {
                             mem_region.add(taint, position.clone());
                         } else {
@@ -184,7 +184,7 @@ impl State {
                 }
             } else {
                 for (mem_id, offset) in pointer.targets().iter() {
-                    if let BitvectorDomain::Value(position) = offset {
+                    if let Ok(position) = offset.try_to_bitvec() {
                         if let Some(mem_region) = self.memory_taint.get_mut(mem_id) {
                             let old_taint = mem_region.get(position.clone(), taint.bytesize());
                             mem_region.add(old_taint.merge(&taint), position.clone());
@@ -239,8 +239,8 @@ impl State {
             for (target, offset) in pointer.targets() {
                 if let Ok(Some(ObjectType::Stack)) = pi_state.memory.get_object_type(target) {
                     // Only check if the value at the address is tainted
-                    if let (Some(mem_object), BitvectorDomain::Value(target_offset)) =
-                        (self.memory_taint.get(target), offset)
+                    if let (Some(mem_object), Ok(target_offset)) =
+                        (self.memory_taint.get(target), offset.try_to_bitvec())
                     {
                         if let Some(taint) = mem_object.get_unsized(target_offset.clone()) {
                             if taint.is_tainted() {
@@ -384,6 +384,7 @@ impl State {
 mod tests {
     use super::*;
     use crate::abstract_domain::*;
+    use crate::analysis::pointer_inference::ValueDomain;
 
     impl State {
         pub fn mock() -> State {
@@ -423,8 +424,8 @@ mod tests {
         }
     }
 
-    fn bv(value: i64) -> BitvectorDomain {
-        BitvectorDomain::Value(Bitvector::from_i64(value))
+    fn bv(value: i64) -> ValueDomain {
+        ValueDomain::from(Bitvector::from_i64(value))
     }
 
     fn new_id(name: &str) -> AbstractIdentifier {
@@ -434,7 +435,7 @@ mod tests {
         )
     }
 
-    fn new_pointer_domain(location: &str, offset: i64) -> PointerDomain<BitvectorDomain> {
+    fn new_pointer_domain(location: &str, offset: i64) -> PointerDomain<ValueDomain> {
         let id = new_id(location);
         PointerDomain::new(id, bv(offset))
     }

src/cwe_checker_lib/src/checkers/cwe_560.rs

@@ -22,7 +22,7 @@
 //! - If the input to umask is not defined in the basic block before the call, the check will not see it.
 //! However, a log message will be generated whenever the check is unable to determine the parameter value of umask.
 
-use crate::abstract_domain::{BitvectorDomain, DataDomain};
+use crate::abstract_domain::TryToBitvec;
 use crate::analysis::pointer_inference::State;
 use crate::intermediate_representation::*;
 use crate::prelude::*;
@@ -72,7 +72,7 @@ fn get_umask_permission_arg(
     let parameter = umask_symbol.get_unique_parameter()?;
     let param_value =
         state.eval_parameter_arg(parameter, &project.stack_pointer_register, global_memory)?;
-    if let DataDomain::Value(BitvectorDomain::Value(umask_arg)) = param_value {
+    if let Ok(umask_arg) = param_value.try_to_bitvec() {
         Ok(umask_arg.try_to_u64()?)
     } else {
         Err(anyhow!("Parameter value unknown"))

src/cwe_checker_lib/src/checkers/cwe_78/context/tests.rs

@@ -2,8 +2,8 @@ use super::*;
 
 use crate::analysis::backward_interprocedural_fixpoint::Context as BackwardContext;
 use crate::{
-    abstract_domain::{BitvectorDomain, DataDomain, PointerDomain, SizedDomain},
-    analysis::pointer_inference::{Data, State as PointerInferenceState},
+    abstract_domain::{DataDomain, PointerDomain, SizedDomain},
+    analysis::pointer_inference::{Data, State as PointerInferenceState, ValueDomain},
     intermediate_representation::{Expression, Variable},
 };
 
@@ -19,8 +19,8 @@ fn mock_block(tid: &str) -> Term<Blk> {
     }
 }
 
-fn bv(value: i64) -> BitvectorDomain {
-    BitvectorDomain::Value(Bitvector::from_i64(value))
+fn bv(value: i64) -> ValueDomain {
+    ValueDomain::from(Bitvector::from_i64(value))
 }
 
 impl ExternSymbol {
@@ -42,8 +42,8 @@ struct Setup {
     pi_state: PointerInferenceState,
     string_sym: ExternSymbol,
     taint_source: Term<Jmp>,
-    base_eight_offset: DataDomain<BitvectorDomain>,
-    base_sixteen_offset: DataDomain<BitvectorDomain>,
+    base_eight_offset: DataDomain<ValueDomain>,
+    base_sixteen_offset: DataDomain<ValueDomain>,
 }
 
 impl Setup {

src/cwe_checker_lib/src/checkers/cwe_78/state/mod.rs

 use std::collections::{HashMap, HashSet};
 
 use crate::{
-    abstract_domain::{
-        AbstractDomain, AbstractIdentifier, BitvectorDomain, MemRegion, SizedDomain,
-    },
+    abstract_domain::{AbstractDomain, AbstractIdentifier, MemRegion, SizedDomain, TryToBitvec},
     analysis::pointer_inference::{Data, State as PointerInferenceState},
     checkers::cwe_476::Taint,
     intermediate_representation::{
@@ -134,7 +132,7 @@ impl State {
         if let Data::Pointer(pointer) = address {
             if pointer.targets().len() == 1 {
                 for (mem_id, offset) in pointer.targets().iter() {
-                    if let BitvectorDomain::Value(position) = offset {
+                    if let Ok(position) = offset.try_to_bitvec() {
                         if let Some(mem_region) = self.memory_taint.get_mut(mem_id) {
                             mem_region.add(taint, position.clone());
                         } else {
@@ -146,7 +144,7 @@ impl State {
                 }
             } else {
                 for (mem_id, offset) in pointer.targets().iter() {
-                    if let BitvectorDomain::Value(position) = offset {
+                    if let Ok(position) = offset.try_to_bitvec() {
                         if let Some(mem_region) = self.memory_taint.get_mut(mem_id) {
                             let old_taint = mem_region.get(position.clone(), taint.bytesize());
                             mem_region.add(old_taint.merge(&taint), position.clone());
@@ -296,8 +294,8 @@ impl State {
     pub fn remove_mem_taint_at_target(&mut self, address: &Data) {
         if let Data::Pointer(pointer) = address {
             for (mem_id, offset) in pointer.targets().iter() {
-                if let (Some(mem_region), BitvectorDomain::Value(position)) =
-                    (self.memory_taint.get_mut(mem_id), offset.clone())
+                if let (Some(mem_region), Ok(position)) =
+                    (self.memory_taint.get_mut(mem_id), offset.try_to_bitvec())
                 {
                     if let Some(taint) = mem_region.get_unsized(position.clone()) {
                         mem_region
@@ -348,8 +346,8 @@ impl State {
             for (target, offset) in pointer.targets() {
                 if let Ok(Some(ObjectType::Stack)) = pi_state.memory.get_object_type(target) {
                     // Only check if the value at the address is tainted
-                    if let (Some(mem_object), BitvectorDomain::Value(target_offset)) =
-                        (self.memory_taint.get(target), offset)
+                    if let (Some(mem_object), Ok(target_offset)) =
+                        (self.memory_taint.get(target), offset.try_to_bitvec())
                     {
                         if let Some(taint) = mem_object.get_unsized(target_offset.clone()) {
                             if taint.is_tainted() {

src/cwe_checker_lib/src/checkers/cwe_78/state/tests.rs

+use crate::analysis::pointer_inference::ValueDomain;
 use crate::{
     abstract_domain::{DataDomain, PointerDomain},
     intermediate_representation::CastOpType,
@@ -17,8 +18,8 @@ fn extern_symbol(name: &str, return_args: Vec<Arg>) -> ExternSymbol {
     }
 }
 
-fn bv(value: i64) -> BitvectorDomain {
-    BitvectorDomain::Value(Bitvector::from_i64(value))
+fn bv(value: i64) -> ValueDomain {
+    ValueDomain::from(Bitvector::from_i64(value))
 }
 
 impl State {
@@ -78,9 +79,9 @@ struct Setup {
     rsp: Variable,
     constant: Bitvector,
     def_tid: Tid,
-    stack_pointer: DataDomain<BitvectorDomain>,
-    base_eight_offset: DataDomain<BitvectorDomain>,
-    base_sixteen_offset: DataDomain<BitvectorDomain>,
+    stack_pointer: DataDomain<ValueDomain>,
+    base_eight_offset: DataDomain<ValueDomain>,
+    base_sixteen_offset: DataDomain<ValueDomain>,
 }
 
 impl Setup {

src/cwe_checker_lib/src/utils/binary.rs

 //! Utility structs and functions which directly parse the binary file.
 
-use crate::abstract_domain::BitvectorDomain;
-use crate::abstract_domain::RegisterDomain;
-use crate::abstract_domain::SizedDomain;
 use crate::intermediate_representation::BinOpType;
+use crate::intermediate_representation::BitvectorExtended;
 use crate::prelude::*;
 use goblin::elf;
 use goblin::pe;
@@ -131,16 +129,16 @@ impl RuntimeMemoryImage {
         }
     }
 
-    /// Read the contents of the memory image at the given address into a `BitvectorDomain`,
+    /// Read the contents of the memory image at the given address
     /// to emulate a read instruction to global data at runtime.
     ///
     /// The read method is endian-aware,
     /// i.e. values are interpreted with the endianness of the CPU architecture.
-    /// If the address points to a writeable segment, the returned value is a `Top` value,
+    /// If the address points to a writeable segment, the returned value is a `Ok(None)` value,
     /// since the data may change during program execution.
     ///
     /// Returns an error if the address is not contained in the global data address range.
-    pub fn read(&self, address: &Bitvector, size: ByteSize) -> Result<BitvectorDomain, Error> {
+    pub fn read(&self, address: &Bitvector, size: ByteSize) -> Result<Option<Bitvector>, Error> {
         let address = address.try_to_u64().unwrap();
         for segment in self.memory_segments.iter() {
             if address >= segment.base_address
@@ -148,7 +146,7 @@ impl RuntimeMemoryImage {
             {
                 if segment.write_flag {
                     // The segment is writeable, thus we do not know the content at runtime.
-                    return Ok(BitvectorDomain::new_top(size));
+                    return Ok(None);
                 }
                 let index = (address - segment.base_address) as usize;
                 let mut bytes = segment.bytes[index..index + u64::from(size) as usize].to_vec();
@@ -156,19 +154,41 @@ impl RuntimeMemoryImage {
                     bytes = bytes.into_iter().rev().collect();
                 }
                 let mut bytes = bytes.into_iter();
-                let mut bitvector: BitvectorDomain =
-                    Bitvector::from_u8(bytes.next().unwrap()).into();
+                let mut bitvector = Bitvector::from_u8(bytes.next().unwrap());
                 for byte in bytes {
-                    let new_byte: BitvectorDomain = Bitvector::from_u8(byte).into();
-                    bitvector = bitvector.bin_op(BinOpType::Piece, &new_byte);
+                    let new_byte = Bitvector::from_u8(byte);
+                    bitvector = bitvector.bin_op(BinOpType::Piece, &new_byte)?;
                 }
-                return Ok(bitvector);
+                return Ok(Some(bitvector));
             }
         }
         // No segment fully contains the read.
         Err(anyhow!("Address is not a valid global memory address."))
     }
 
+    /// Check whether all addresses in the given interval point to a readable segment in the runtime memory image.
+    ///
+    /// Returns an error if the address interval intersects more than one memory segment
+    /// or if it does not point to global memory at all.
+    pub fn is_interval_readable(
+        &self,
+        start_address: u64,
+        end_address: u64,
+    ) -> Result<bool, Error> {
+        for segment in self.memory_segments.iter() {
+            if start_address >= segment.base_address
+                && start_address < segment.base_address + segment.bytes.len() as u64
+            {
+                if end_address <= segment.base_address + segment.bytes.len() as u64 {
+                    return Ok(segment.read_flag);
+                } else {
+                    return Err(anyhow!("Interval spans more than one segment"));
+                }
+            }
+        }
+        Err(anyhow!("Address not contained in runtime memory image"))
+    }
+
     /// For an address to global read-only memory, return the memory segment it points to
     /// and the index inside the segment, where the address points to.
     ///
@@ -207,6 +227,29 @@ impl RuntimeMemoryImage {
         }
         Err(anyhow!("Address not contained in runtime memory image"))
     }
+
+    /// Check whether all addresses in the given interval point to a writeable segment in the runtime memory image.
+    ///
+    /// Returns an error if the address interval intersects more than one memory segment
+    /// or if it does not point to global memory at all.
+    pub fn is_interval_writeable(
+        &self,
+        start_address: u64,
+        end_address: u64,
+    ) -> Result<bool, Error> {
+        for segment in self.memory_segments.iter() {
+            if start_address >= segment.base_address
+                && start_address < segment.base_address + segment.bytes.len() as u64
+            {
+                if end_address <= segment.base_address + segment.bytes.len() as u64 {
+                    return Ok(segment.write_flag);
+                } else {
+                    return Err(anyhow!("Interval spans more than one segment"));
+                }
+            }
+        }
+        Err(anyhow!("Address not contained in runtime memory image"))
+    }
 }
 
 #[cfg(test)]