Enum cwe_checker_lib::abstract_domain::BricksDomain

pub enum BricksDomain {
    Top,
    Value(Vec<BrickDomain>),
}

The BricksDomain contains a sorted list of single normalized BrickDomains. It represents the composition of a string through sub sequences.

Variants

Top

The Top value represents an invalid sequence.

Value(Vec<BrickDomain>)

This values represents a sequence of string subsequences.

Implementations

impl BricksDomain

pub fn widen(&self, other: &BricksDomain) -> Self

The widen function of the BricksDomain widens the values during a merge. If the two BrickDomain lists are not comparable or either list exceeds the length threshold, Top is returned. Otherwise, the shorter list is padded and the widen function of the BrickDomain is applied to each element in both lists. If after the widening all BrickDomain values are Top, return the Top value for the BricksDomain.

pub fn all_bricks_are_top(bricks: &[BrickDomain]) -> bool

Checks whether all bricks of the BricksDomain are Top values. If so, the BricksDomain itself should be converted into a Top value.

pub fn is_less_or_equal(&self, other: &BricksDomain) -> bool

Checks whether the current BricksDomain is less or equal than the other BricksDomain by definition of the partial order.

impl BricksDomain

pub fn normalize(&self) -> Self

A set of strings can be built from multiple configurations of bricks e.g. [{abc}]^{1,1} <=> [{a}]^{1,1}[{b}]^{1,1}[{c}]^{1,1}

Introducing a normalized form [T]^{1,1} or [T]^{0, max>0} will keep string representations unambiguous.

Normalizing can be seen as some kind of fixpoint for a set of 5 rules that are applied to the list of bricks until the state stays unchanged:

1. remove bricks of the form [{}]^{0,0} empty string
2. merge successive bricks with the same indices max = 1, min = 1, in a new single brick. The new string set is the concatenation of the former two. e.g. B0 = [{a,cd}]^{1,1} and B1 = [{b,ef}]^{1,1} become B_new = [{ab, aef, cdb, cdef}]^{1,1}.
3. transform a brick in which the number of applications is constant (min = max) into one in which min = max = 1. e.g. B = [{a,b}]^{2,2} => B_new = [{aa, ab, ba, bb}]^{1,1}.
4. merge two successive bricks in which the set of strings is the same. e.g. B1 = [S]^{m1, M1} and B2 = [S]^{m2, M2} => B_new = [S]^{m1+m2, M1+M2}
5. break a single brick with min >= 1 and max != min into two simpler bricks where B = [S]^{min,max} => B1 = [S^min]^{1,1}, B2 = [S]^{0, max-min}. e.g. B = [{a}]^{2,5} => B1 = [{aa}]^{1,1}, B2 = [{a}]^{0,3}

Since normalization is rather expensive w.r.t. runtime and since it could entail a precision loss, it is only computed after a merge or widening operation.

Trait Implementations

impl AbstractDomain for BricksDomain

fn merge(&self, other: &Self) -> Self

Takes care of merging lists of bricks

fn is_top(&self) -> bool

Check if the value is Top.

fn merge_with(&mut self, other: &Self) -> &mut Self

Returns an upper bound (with respect to the partial order on the domain) for the two inputs self and other.

impl Clone for BricksDomain

fn clone(&self) -> BricksDomain

Returns a copy of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for BricksDomain

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl<'de> Deserialize<'de> for BricksDomain

fn deserialize<__D>(__deserializer: __D) -> Result<Self, __D::Error>

where __D: Deserializer<'de>,

Deserialize this value from the given Serde deserializer.

impl Display for BricksDomain

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl DomainInsertion for BricksDomain

fn append_string_domain(&self, string_domain: &Self) -> Self

Appends new bricks to the current BricksDomain. Used to insert format specifier in sprintf calls and for strcat call.

fn create_float_value_domain() -> Self

Create a string domain that approximates float values.

fn create_char_domain() -> Self

Create a string domain that approximates char values.

fn create_integer_domain() -> Self

Create a string domain that approximates integer values.

fn create_pointer_value_domain() -> Self

Create a string domain that approximates pointer values.

fn create_top_value_domain() -> Self

Creates a top value of the domain.

fn create_empty_string_domain() -> Self

Create a string domain that represents an empty string.

impl From<String> for BricksDomain

fn from(string: String) -> Self

Returns a new instance of the Bricks Domain

impl HasTop for BricksDomain

fn top(&self) -> Self

Return a Top value

impl PartialEq for BricksDomain

fn eq(&self, other: &BricksDomain) -> bool

This method tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

This method tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl Serialize for BricksDomain

fn serialize<__S>(&self, __serializer: __S) -> Result<__S::Ok, __S::Error>

where __S: Serializer,

Serialize this value into the given Serde serializer.

impl Eq for BricksDomain

impl StructuralEq for BricksDomain

impl StructuralPartialEq for BricksDomain