1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154

//! This module implements the widening operator for the BrickDomain and BricksDomain.
//! The exact widening procedure depends on three constants.
//!  - The *interval threshold* overapproximates the number of times string sequences can occur in a brick.
//!  - The *sequence threshold* overapproximates the number of string sequences in a brick by forcing a *Top* value.
//!  - The *length threshold* overapproximates the number of bricks in the BricksDomain and forces a *Top* value.
//! A merge is processed without widening when none of the thresholds are exceeded.

use std::{
    cmp::{
        max, min,
        Ordering::{Equal, Greater, Less},
    },
    collections::BTreeSet,
};

use crate::abstract_domain::AbstractDomain;

use super::{brick::Brick, BrickDomain, BricksDomain};

pub const INTERVAL_THRESHOLD: usize = 8;
pub const SEQUENCE_THRESHOLD: usize = 8;
pub const LENGTH_THRESHOLD: usize = 32;

impl BricksDomain {
    /// 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 widen(&self, other: &BricksDomain) -> Self {
        let self_num_of_bricks = self.unwrap_value().len();
        let other_num_of_bricks = other.unwrap_value().len();

        let mut new_self = self.clone();
        let mut new_other = other.clone();

        match self_num_of_bricks.cmp(&other_num_of_bricks) {
            Less => {
                new_self = self.pad_list(other);
            }
            Greater => {
                new_other = other.pad_list(self);
            }
            Equal => (),
        }

        if !new_self.is_less_or_equal(other) && !new_other.is_less_or_equal(self)
            || self_num_of_bricks > LENGTH_THRESHOLD
            || other_num_of_bricks > LENGTH_THRESHOLD
        {
            return BricksDomain::Top;
        }

        let mut widened_brick_domain_list: Vec<BrickDomain> = Vec::new();

        for (self_brick, other_brick) in new_self
            .unwrap_value()
            .iter()
            .zip(new_other.unwrap_value().iter())
        {
            widened_brick_domain_list.push(self_brick.merge(other_brick));
        }

        if BricksDomain::all_bricks_are_top(&widened_brick_domain_list) {
            return BricksDomain::Top;
        }

        BricksDomain::Value(widened_brick_domain_list)
    }

    /// Checks whether all bricks of the BricksDomain are *Top* values.
    /// If so, the BricksDomain itself should be converted into a *Top* value.
    pub fn all_bricks_are_top(bricks: &[BrickDomain]) -> bool {
        bricks.iter().all(|brick| matches!(brick, BrickDomain::Top))
    }

    /// Checks whether the current BricksDomain is less or equal than the other BricksDomain
    /// by definition of the partial order.
    pub fn is_less_or_equal(&self, other: &BricksDomain) -> bool {
        self.unwrap_value()
            .iter()
            .zip(other.unwrap_value().iter())
            .all(|(self_brick, other_brick)| self_brick.is_less_or_equal(other_brick))
    }
}

impl BrickDomain {
    /// The widen function of the BrickDomain takes the union of both
    /// BrickDomains and returns *Top* if the number of sequences exceeds
    /// a certain threshold.
    /// If neither of the domains are *Top*, the minimum and maximum
    /// of the interval bounds are taken and it is checked whether
    /// their difference exceeds a certain threshold.
    /// If so *min* is set to 0 and *max* is set to infinity (here Max value of 32 bits).
    /// Otherwise, their values are taken as new bounds for the merged domain.
    pub fn widen(&self, other: &BrickDomain) -> Self {
        let self_brick = self.unwrap_value();
        let other_brick = other.unwrap_value();
        let merged_sequence = self_brick
            .get_sequence()
            .union(other_brick.get_sequence())
            .cloned()
            .collect::<BTreeSet<String>>();

        if merged_sequence.len() > SEQUENCE_THRESHOLD {
            return BrickDomain::Top;
        }

        let mut widened_brick = Brick::new();
        let min_bound = min(self_brick.get_min(), other_brick.get_min());
        let max_bound = max(self_brick.get_max(), other_brick.get_max());

        if max_bound - min_bound > INTERVAL_THRESHOLD as u32 {
            widened_brick.set_min(0);
            widened_brick.set_max(u32::MAX);
        } else {
            widened_brick.set_min(min_bound);
            widened_brick.set_max(max_bound);
        }

        widened_brick.set_sequence(merged_sequence);

        BrickDomain::Value(widened_brick)
    }

    /// Checks whether the current BrickDomain is less or equal than the other BrickDomain
    /// by definition of the partial order.
    /// Empty strings are ignored for order comparisons.
    pub fn is_less_or_equal(&self, other: &BrickDomain) -> bool {
        match (self.is_top(), other.is_top()) {
            (false, false) => {
                let self_brick = self.unwrap_value();
                let other_brick = other.unwrap_value();
                if self_brick.is_empty_string() || other_brick.is_empty_string() {
                    return true;
                }
                if self_brick
                    .get_sequence()
                    .is_subset(other_brick.get_sequence())
                    && self_brick.get_min() >= other_brick.get_min()
                    && self_brick.get_max() <= other_brick.get_max()
                {
                    return true;
                }

                false
            }
            (true, false) => false,
            (false, true) | (true, true) => true,
        }
    }
}