1use std::collections::BTreeSet;
2
3use crate::automaton::{automaton_class_value_from_owned_values, automaton_is_well_formed_acyclic};
4use crate::{
5 ABSTRACT_VALUE_CASCADE_FAMILY_CLAIM_LEVEL_V0, AbstractClassValueProvenanceV0,
6 AbstractClassValueV0, AbstractValueDomainSummaryV0, CompositeClassValueInputV0, FactPrecision,
7 MAX_FINITE_CLASS_VALUES, OmenaAbstractValueCoverageDirectionV0,
8 OmenaAbstractValuePrecisionBasisV0, OmenaAbstractValuePrecisionWitnessV0,
9};
10
11pub fn summarize_omena_abstract_value_domain() -> AbstractValueDomainSummaryV0 {
12 AbstractValueDomainSummaryV0 {
13 schema_version: "0",
14 product: "omena-abstract-value.domain",
15 domain_kinds: vec![
16 "bottom",
17 "exact",
18 "finiteSet",
19 "automaton",
20 "prefix",
21 "suffix",
22 "prefixSuffix",
23 "charInclusion",
24 "composite",
25 "propertyValue",
26 "top",
27 ],
28 max_finite_class_values: MAX_FINITE_CLASS_VALUES,
29 reduced_product_structure_ready: true,
30 reduced_product_axes: vec!["prefix", "suffix", "charInclusion", "lengthLowerBound"],
31 reduced_product_operations: vec!["intersect", "join", "concat", "subset", "matchesString"],
32 reduced_product_consumers: vec![
33 "selectorProjection",
34 "expressionDomainFlow",
35 "semanticReachability",
36 "treeShakeClass",
37 ],
38 selector_projection_certainties: vec!["exact", "inferred", "possible"],
39 provenance_tree_ready: true,
40 provenance_tree_scopes: vec![
41 "literal",
42 "finiteSet",
43 "constraint",
44 "finiteSetWidening",
45 "reducedProduct",
46 "flowResult",
47 ],
48 cascade_family_substrate_ready: true,
49 cascade_family_framing: "framingNeutralCascadeFamily",
50 cascade_family_claim_level: ABSTRACT_VALUE_CASCADE_FAMILY_CLAIM_LEVEL_V0,
51 }
52}
53
54pub fn bottom_class_value() -> AbstractClassValueV0 {
55 AbstractClassValueV0::Bottom
56}
57
58pub fn top_class_value() -> AbstractClassValueV0 {
59 top_class_value_with_provenance(AbstractClassValueProvenanceV0::UnconstrainedInput)
60}
61
62pub fn top_class_value_with_provenance(
63 provenance: AbstractClassValueProvenanceV0,
64) -> AbstractClassValueV0 {
65 AbstractClassValueV0::Top {
66 provenance: Some(provenance),
67 }
68}
69
70pub fn exact_class_value(value: impl Into<String>) -> AbstractClassValueV0 {
71 AbstractClassValueV0::Exact {
72 value: value.into(),
73 }
74}
75
76pub fn finite_set_class_value<I, S>(values: I) -> AbstractClassValueV0
77where
78 I: IntoIterator<Item = S>,
79 S: Into<String>,
80{
81 automaton_class_value_from_owned_values(
82 values.into_iter().map(Into::into),
83 Some(AbstractClassValueProvenanceV0::FiniteSetWideningAutomaton),
84 )
85}
86
87pub fn prefix_class_value(
88 prefix: impl Into<String>,
89 provenance: Option<AbstractClassValueProvenanceV0>,
90) -> AbstractClassValueV0 {
91 AbstractClassValueV0::Prefix {
92 prefix: prefix.into(),
93 provenance,
94 }
95}
96
97pub fn suffix_class_value(
98 suffix: impl Into<String>,
99 provenance: Option<AbstractClassValueProvenanceV0>,
100) -> AbstractClassValueV0 {
101 AbstractClassValueV0::Suffix {
102 suffix: suffix.into(),
103 provenance,
104 }
105}
106
107pub fn prefix_suffix_class_value(
108 prefix: impl Into<String>,
109 suffix: impl Into<String>,
110 min_length: Option<usize>,
111 provenance: Option<AbstractClassValueProvenanceV0>,
112) -> AbstractClassValueV0 {
113 let prefix = prefix.into();
114 let suffix = suffix.into();
115 if prefix.is_empty() && suffix.is_empty() {
116 return top_class_value();
117 }
118 if prefix.is_empty() {
119 return suffix_class_value(suffix, provenance);
120 }
121 if suffix.is_empty() {
122 return prefix_class_value(prefix, provenance);
123 }
124
125 AbstractClassValueV0::PrefixSuffix {
126 min_length: min_length
127 .unwrap_or_else(|| prefix_suffix_min_length(&prefix, &suffix))
128 .max(prefix_suffix_min_length(&prefix, &suffix)),
129 prefix,
130 suffix,
131 provenance,
132 }
133}
134
135pub fn char_inclusion_class_value(
136 must_chars: impl Into<String>,
137 may_chars: impl Into<String>,
138 provenance: Option<AbstractClassValueProvenanceV0>,
139 may_include_other_chars: bool,
140) -> AbstractClassValueV0 {
141 let must_chars = normalize_char_set(must_chars.into());
142 let may_chars = normalize_char_set(format!("{}{}", may_chars.into(), must_chars));
143
144 if may_include_other_chars && must_chars.is_empty() {
145 return top_class_value();
146 }
147 if !may_include_other_chars && may_chars.is_empty() {
148 return bottom_class_value();
149 }
150
151 AbstractClassValueV0::CharInclusion {
152 must_chars,
153 may_chars,
154 may_include_other_chars,
155 provenance,
156 }
157}
158
159pub fn composite_class_value(input: CompositeClassValueInputV0) -> AbstractClassValueV0 {
160 let prefix = input.prefix.unwrap_or_default();
161 let suffix = input.suffix.unwrap_or_default();
162 let edge_chars = char_set_for_string(format!("{prefix}{suffix}"));
163 let must_chars = normalize_char_set(format!("{}{}", input.must_chars, edge_chars));
164 let may_chars = normalize_char_set(format!("{}{}", input.may_chars, must_chars));
165 let has_char_info =
166 !must_chars.is_empty() || (!input.may_include_other_chars && !may_chars.is_empty());
167
168 if !has_char_info {
169 return prefix_suffix_class_value(prefix, suffix, input.min_length, input.provenance);
170 }
171 if prefix.is_empty() && suffix.is_empty() {
172 return char_inclusion_class_value(
173 must_chars,
174 may_chars,
175 input.provenance,
176 input.may_include_other_chars,
177 );
178 }
179
180 let minimum_length = composite_min_length_for_constraints(&prefix, &suffix, &must_chars);
181 let min_length = input
182 .min_length
183 .map(|value| value.max(minimum_length))
184 .or(Some(minimum_length));
185
186 AbstractClassValueV0::Composite {
187 prefix: (!prefix.is_empty()).then_some(prefix),
188 suffix: (!suffix.is_empty()).then_some(suffix),
189 min_length,
190 must_chars,
191 may_chars,
192 may_include_other_chars: input.may_include_other_chars,
193 provenance: input.provenance,
194 }
195}
196
197pub fn enumerate_finite_class_values(value: &AbstractClassValueV0) -> Option<Vec<String>> {
198 match value {
199 AbstractClassValueV0::Bottom => Some(Vec::new()),
200 AbstractClassValueV0::Exact { value } => Some(vec![value.clone()]),
201 AbstractClassValueV0::FiniteSet { values } => Some(values.clone()),
202 AbstractClassValueV0::Automaton { .. } => None,
203 _ => None,
204 }
205}
206
207pub fn abstract_class_value_kind(value: &AbstractClassValueV0) -> &'static str {
208 match value {
209 AbstractClassValueV0::Bottom => "bottom",
210 AbstractClassValueV0::Exact { .. } => "exact",
211 AbstractClassValueV0::FiniteSet { .. } => "finiteSet",
212 AbstractClassValueV0::Automaton { .. } => "automaton",
213 AbstractClassValueV0::Prefix { .. } => "prefix",
214 AbstractClassValueV0::Suffix { .. } => "suffix",
215 AbstractClassValueV0::PrefixSuffix { .. } => "prefixSuffix",
216 AbstractClassValueV0::CharInclusion { .. } => "charInclusion",
217 AbstractClassValueV0::Composite { .. } => "composite",
218 AbstractClassValueV0::Top { .. } => "top",
219 }
220}
221
222pub fn fact_precision_from_class_value(value: &AbstractClassValueV0) -> FactPrecision {
223 fact_precision_from_class_value_with_witness(value, None)
224}
225
226pub fn fact_precision_from_class_value_with_witness(
227 value: &AbstractClassValueV0,
228 external_witness: Option<&OmenaAbstractValuePrecisionWitnessV0>,
229) -> FactPrecision {
230 match value {
231 AbstractClassValueV0::Bottom | AbstractClassValueV0::Exact { .. } => FactPrecision::Exact,
232 AbstractClassValueV0::FiniteSet { values }
233 if closed_set_precision_witness_is_sound(values, external_witness) =>
234 {
235 FactPrecision::Exact
236 }
237 AbstractClassValueV0::FiniteSet { .. } => FactPrecision::Conservative,
238 AbstractClassValueV0::Automaton {
239 automaton,
240 precision_witness,
241 ..
242 } if automaton_precision_witness_is_sound(automaton, precision_witness.as_ref()) => {
243 FactPrecision::Conservative
244 }
245 AbstractClassValueV0::Automaton { .. }
246 | AbstractClassValueV0::Prefix { .. }
247 | AbstractClassValueV0::Suffix { .. }
248 | AbstractClassValueV0::PrefixSuffix { .. }
249 | AbstractClassValueV0::CharInclusion { .. }
250 | AbstractClassValueV0::Composite { .. } => FactPrecision::Heuristic,
251 AbstractClassValueV0::Top { .. } => FactPrecision::Unknown,
252 }
253}
254
255fn automaton_precision_witness_is_sound(
256 automaton: &crate::AbstractStringAutomatonV0,
257 witness: Option<&OmenaAbstractValuePrecisionWitnessV0>,
258) -> bool {
259 matches!(
260 witness,
261 Some(OmenaAbstractValuePrecisionWitnessV0 {
262 direction: OmenaAbstractValueCoverageDirectionV0::SupersetOfProducible,
263 basis: OmenaAbstractValuePrecisionBasisV0::AcyclicExact,
264 authority_digest: None,
265 })
266 ) && automaton_is_well_formed_acyclic(automaton)
267}
268
269fn closed_set_precision_witness_is_sound(
270 values: &[String],
271 witness: Option<&OmenaAbstractValuePrecisionWitnessV0>,
272) -> bool {
273 (2..=MAX_FINITE_CLASS_VALUES).contains(&values.len())
274 && matches!(
275 witness,
276 Some(OmenaAbstractValuePrecisionWitnessV0 {
277 direction: OmenaAbstractValueCoverageDirectionV0::SupersetOfProducible,
278 basis: OmenaAbstractValuePrecisionBasisV0::ClosedSetEnumeration,
279 authority_digest: Some(authority_digest),
280 }) if !authority_digest.is_empty()
281 )
282}
283
284pub(crate) fn normalize_char_set(chars: impl AsRef<str>) -> String {
285 chars
286 .as_ref()
287 .chars()
288 .collect::<BTreeSet<_>>()
289 .into_iter()
290 .collect()
291}
292
293pub(crate) fn union_char_sets(left: &str, right: &str) -> String {
294 normalize_char_set(format!("{left}{right}"))
295}
296
297pub(crate) fn intersect_char_sets(left: &str, right: &str) -> String {
298 let right_set = right.chars().collect::<BTreeSet<_>>();
299 left.chars()
300 .filter(|char| right_set.contains(char))
301 .collect::<BTreeSet<_>>()
302 .into_iter()
303 .collect()
304}
305
306pub(crate) fn char_set_for_string(value: impl AsRef<str>) -> String {
307 normalize_char_set(value)
308}
309
310pub(crate) fn meaningful_longest_common_prefix(values: &[String]) -> String {
311 let prefix = longest_common_prefix(values);
312 if prefix.is_empty() || !is_meaningful_class_prefix(&prefix, values) {
313 return String::new();
314 }
315 prefix
316}
317
318pub(crate) fn meaningful_longest_common_suffix(values: &[String]) -> String {
319 let suffix = longest_common_suffix(values);
320 if suffix.is_empty() || !is_meaningful_class_suffix(&suffix, values) {
321 return String::new();
322 }
323 suffix
324}
325
326pub(crate) fn char_set_is_subset(left: &str, right: &str) -> bool {
327 let right = right.chars().collect::<BTreeSet<_>>();
328 left.chars().all(|char| right.contains(&char))
329}
330
331pub(crate) fn prefix_suffix_min_length(prefix: &str, suffix: &str) -> usize {
332 prefix.len() + suffix.len() - prefix_suffix_overlap_len(prefix, suffix)
333}
334
335pub(crate) fn composite_min_length_for_constraints(
336 prefix: &str,
337 suffix: &str,
338 must_chars: &str,
339) -> usize {
340 let edge_chars = char_set_for_string(format!("{prefix}{suffix}"));
341 let missing_required_char_len = must_chars
342 .chars()
343 .filter(|char| !edge_chars.contains(*char))
344 .map(char::len_utf8)
345 .sum::<usize>();
346
347 if missing_required_char_len == 0 {
348 prefix_suffix_min_length(prefix, suffix)
349 } else {
350 prefix.len() + suffix.len() + missing_required_char_len
351 }
352}
353
354pub(crate) fn prefix_suffix_overlap_len(prefix: &str, suffix: &str) -> usize {
355 let max_overlap = prefix.len().min(suffix.len());
356
357 for overlap in (0..=max_overlap).rev() {
358 let prefix_start = prefix.len() - overlap;
359 if prefix.is_char_boundary(prefix_start)
360 && suffix.is_char_boundary(overlap)
361 && prefix[prefix_start..] == suffix[..overlap]
362 {
363 return overlap;
364 }
365 }
366
367 0
368}
369
370fn longest_common_prefix(values: &[String]) -> String {
371 let Some(first) = values.first() else {
372 return String::new();
373 };
374 let mut prefix = first.clone();
375
376 for value in values.iter().skip(1) {
377 let mut match_length = 0usize;
378 for (left, right) in prefix.chars().zip(value.chars()) {
379 if left != right {
380 break;
381 }
382 match_length += left.len_utf8();
383 }
384 prefix.truncate(match_length);
385 if prefix.is_empty() {
386 break;
387 }
388 }
389
390 prefix
391}
392
393fn longest_common_suffix(values: &[String]) -> String {
394 let reversed = values
395 .iter()
396 .map(|value| value.chars().rev().collect::<String>())
397 .collect::<Vec<_>>();
398 longest_common_prefix(&reversed)
399 .chars()
400 .rev()
401 .collect::<String>()
402}
403
404fn is_meaningful_class_prefix(prefix: &str, values: &[String]) -> bool {
405 if prefix.is_empty() {
406 return false;
407 }
408 if ends_at_class_boundary(prefix) {
409 return true;
410 }
411 values.iter().all(|value| {
412 value.len() == prefix.len()
413 || value[prefix.len()..]
414 .chars()
415 .next()
416 .is_some_and(is_class_boundary_char)
417 })
418}
419
420fn is_meaningful_class_suffix(suffix: &str, values: &[String]) -> bool {
421 if suffix.is_empty() {
422 return false;
423 }
424 if starts_at_class_boundary(suffix) {
425 return true;
426 }
427 values.iter().all(|value| {
428 if value.len() == suffix.len() {
429 return true;
430 }
431 value[..value.len() - suffix.len()]
432 .chars()
433 .next_back()
434 .is_some_and(is_class_boundary_char)
435 })
436}
437
438fn ends_at_class_boundary(value: &str) -> bool {
439 value
440 .chars()
441 .next_back()
442 .is_some_and(is_class_boundary_char)
443}
444
445fn starts_at_class_boundary(value: &str) -> bool {
446 value.chars().next().is_some_and(is_class_boundary_char)
447}
448
449fn is_class_boundary_char(char: char) -> bool {
450 char == '-' || char == '_'
451}