pmat 3.11.0

PMAT - Zero-config AI context generation and code quality toolkit (CLI, MCP, HTTP)
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

// Lattice impl blocks for abstract domain types:
// PropertyDomain (top, join, widen, is_equal),
// NullabilityLattice (join), IntervalLattice (widen, is_equal),
// AliasLattice (join), PurityLattice (meet).

impl PropertyDomain {
    /// Create a top (unknown) property domain
    ///
    /// # Examples
    ///
    /// ```
    /// use pmat::services::lightweight_provability_analyzer::PropertyDomain;
    ///
    /// let domain = PropertyDomain::top();
    /// // All properties are initially unknown
    /// ```
    #[must_use]
    pub fn top() -> Self {
        Self {
            nullability: NullabilityLattice::Top,
            bounds: IntervalLattice {
                lower: None,
                upper: None,
            },
            aliasing: AliasLattice::Top,
            purity: PurityLattice::Top,
        }
    }

    #[must_use]
    pub fn join(&self, other: &Self) -> Self {
        Self {
            nullability: self.nullability.join(&other.nullability),
            bounds: self.bounds.widen(&other.bounds),
            aliasing: self.aliasing.join(&other.aliasing),
            purity: self.purity.meet(&other.purity),
        }
    }

    #[must_use]
    pub fn widen(&self, other: &Self) -> Self {
        Self {
            nullability: self.nullability.join(&other.nullability),
            bounds: self.bounds.widen(&other.bounds),
            aliasing: self.aliasing.join(&other.aliasing),
            purity: self.purity.meet(&other.purity),
        }
    }

    #[must_use]
    pub fn is_equal(&self, other: &Self) -> bool {
        self.nullability == other.nullability
            && self.bounds.is_equal(&other.bounds)
            && self.aliasing == other.aliasing
            && self.purity == other.purity
    }
}

impl NullabilityLattice {
    #[must_use]
    pub fn join(&self, other: &Self) -> Self {
        use NullabilityLattice::{Bottom, MaybeNull, NotNull, Null, Top};
        match (self, other) {
            (Bottom, x) | (x, Bottom) => x.clone(),
            (Top, _) | (_, Top) => Top,
            (NotNull, NotNull) => NotNull,
            (Null, Null) => Null,
            (NotNull, Null) | (Null, NotNull) => Bottom, // Contradiction
            _ => MaybeNull,
        }
    }
}

impl IntervalLattice {
    #[must_use]
    pub fn widen(&self, other: &Self) -> Self {
        let lower = match (self.lower, other.lower) {
            (Some(a), Some(b)) if a > b => None, // Widening to -inf
            (l, _) => l,
        };

        let upper = match (self.upper, other.upper) {
            (Some(a), Some(b)) if a < b => None, // Widening to +inf
            (u, _) => u,
        };

        Self { lower, upper }
    }

    #[must_use]
    pub fn is_equal(&self, other: &Self) -> bool {
        self.lower == other.lower && self.upper == other.upper
    }
}

impl AliasLattice {
    #[must_use]
    pub fn join(&self, other: &Self) -> Self {
        use AliasLattice::{Bottom, MayAlias, MustAlias, NoAlias, Top};
        match (self, other) {
            (Bottom, x) | (x, Bottom) => x.clone(),
            (Top, _) | (_, Top) => Top,
            (NoAlias, NoAlias) => NoAlias,
            (MustAlias, MustAlias) => MustAlias,
            _ => MayAlias,
        }
    }
}

impl PurityLattice {
    #[must_use]
    pub fn meet(&self, other: &Self) -> Self {
        use PurityLattice::{Bottom, Pure, ReadOnly, Top, WriteGlobal, WriteLocal};
        match (self, other) {
            (Bottom, _) | (_, Bottom) => Bottom,
            (WriteGlobal, _) | (_, WriteGlobal) => WriteGlobal,
            (WriteLocal, _) | (_, WriteLocal) => WriteLocal,
            (ReadOnly, ReadOnly) => ReadOnly,
            (Pure, Pure) => Pure,
            _ => Top,
        }
    }
}