1use std::collections::BTreeSet;
2
3use crate::automaton::{automaton_class_value_from_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 let normalized = normalize_values(values);
82 match normalized.len() {
83 0 => bottom_class_value(),
84 1 => exact_class_value(normalized[0].clone()),
85 2..=MAX_FINITE_CLASS_VALUES => AbstractClassValueV0::FiniteSet { values: normalized },
86 _ => automaton_class_value_from_values(
87 &normalized,
88 Some(AbstractClassValueProvenanceV0::FiniteSetWideningAutomaton),
89 ),
90 }
91}
92
93pub fn prefix_class_value(
94 prefix: impl Into<String>,
95 provenance: Option<AbstractClassValueProvenanceV0>,
96) -> AbstractClassValueV0 {
97 AbstractClassValueV0::Prefix {
98 prefix: prefix.into(),
99 provenance,
100 }
101}
102
103pub fn suffix_class_value(
104 suffix: impl Into<String>,
105 provenance: Option<AbstractClassValueProvenanceV0>,
106) -> AbstractClassValueV0 {
107 AbstractClassValueV0::Suffix {
108 suffix: suffix.into(),
109 provenance,
110 }
111}
112
113pub fn prefix_suffix_class_value(
114 prefix: impl Into<String>,
115 suffix: impl Into<String>,
116 min_length: Option<usize>,
117 provenance: Option<AbstractClassValueProvenanceV0>,
118) -> AbstractClassValueV0 {
119 let prefix = prefix.into();
120 let suffix = suffix.into();
121 if prefix.is_empty() && suffix.is_empty() {
122 return top_class_value();
123 }
124 if prefix.is_empty() {
125 return suffix_class_value(suffix, provenance);
126 }
127 if suffix.is_empty() {
128 return prefix_class_value(prefix, provenance);
129 }
130
131 AbstractClassValueV0::PrefixSuffix {
132 min_length: min_length
133 .unwrap_or_else(|| prefix_suffix_min_length(&prefix, &suffix))
134 .max(prefix_suffix_min_length(&prefix, &suffix)),
135 prefix,
136 suffix,
137 provenance,
138 }
139}
140
141pub fn char_inclusion_class_value(
142 must_chars: impl Into<String>,
143 may_chars: impl Into<String>,
144 provenance: Option<AbstractClassValueProvenanceV0>,
145 may_include_other_chars: bool,
146) -> AbstractClassValueV0 {
147 let must_chars = normalize_char_set(must_chars.into());
148 let may_chars = normalize_char_set(format!("{}{}", may_chars.into(), must_chars));
149
150 if may_include_other_chars && must_chars.is_empty() {
151 return top_class_value();
152 }
153 if !may_include_other_chars && may_chars.is_empty() {
154 return bottom_class_value();
155 }
156
157 AbstractClassValueV0::CharInclusion {
158 must_chars,
159 may_chars,
160 may_include_other_chars,
161 provenance,
162 }
163}
164
165pub fn composite_class_value(input: CompositeClassValueInputV0) -> AbstractClassValueV0 {
166 let prefix = input.prefix.unwrap_or_default();
167 let suffix = input.suffix.unwrap_or_default();
168 let edge_chars = char_set_for_string(format!("{prefix}{suffix}"));
169 let must_chars = normalize_char_set(format!("{}{}", input.must_chars, edge_chars));
170 let may_chars = normalize_char_set(format!("{}{}", input.may_chars, must_chars));
171 let has_char_info =
172 !must_chars.is_empty() || (!input.may_include_other_chars && !may_chars.is_empty());
173
174 if !has_char_info {
175 return prefix_suffix_class_value(prefix, suffix, input.min_length, input.provenance);
176 }
177 if prefix.is_empty() && suffix.is_empty() {
178 return char_inclusion_class_value(
179 must_chars,
180 may_chars,
181 input.provenance,
182 input.may_include_other_chars,
183 );
184 }
185
186 let minimum_length = composite_min_length_for_constraints(&prefix, &suffix, &must_chars);
187 let min_length = input
188 .min_length
189 .map(|value| value.max(minimum_length))
190 .or(Some(minimum_length));
191
192 AbstractClassValueV0::Composite {
193 prefix: (!prefix.is_empty()).then_some(prefix),
194 suffix: (!suffix.is_empty()).then_some(suffix),
195 min_length,
196 must_chars,
197 may_chars,
198 may_include_other_chars: input.may_include_other_chars,
199 provenance: input.provenance,
200 }
201}
202
203pub fn enumerate_finite_class_values(value: &AbstractClassValueV0) -> Option<Vec<String>> {
204 match value {
205 AbstractClassValueV0::Bottom => Some(Vec::new()),
206 AbstractClassValueV0::Exact { value } => Some(vec![value.clone()]),
207 AbstractClassValueV0::FiniteSet { values } => Some(values.clone()),
208 AbstractClassValueV0::Automaton { .. } => None,
209 _ => None,
210 }
211}
212
213pub fn abstract_class_value_kind(value: &AbstractClassValueV0) -> &'static str {
214 match value {
215 AbstractClassValueV0::Bottom => "bottom",
216 AbstractClassValueV0::Exact { .. } => "exact",
217 AbstractClassValueV0::FiniteSet { .. } => "finiteSet",
218 AbstractClassValueV0::Automaton { .. } => "automaton",
219 AbstractClassValueV0::Prefix { .. } => "prefix",
220 AbstractClassValueV0::Suffix { .. } => "suffix",
221 AbstractClassValueV0::PrefixSuffix { .. } => "prefixSuffix",
222 AbstractClassValueV0::CharInclusion { .. } => "charInclusion",
223 AbstractClassValueV0::Composite { .. } => "composite",
224 AbstractClassValueV0::Top { .. } => "top",
225 }
226}
227
228pub fn fact_precision_from_class_value(value: &AbstractClassValueV0) -> FactPrecision {
229 fact_precision_from_class_value_with_witness(value, None)
230}
231
232pub fn fact_precision_from_class_value_with_witness(
233 value: &AbstractClassValueV0,
234 external_witness: Option<&OmenaAbstractValuePrecisionWitnessV0>,
235) -> FactPrecision {
236 match value {
237 AbstractClassValueV0::Bottom | AbstractClassValueV0::Exact { .. } => FactPrecision::Exact,
238 AbstractClassValueV0::FiniteSet { values }
239 if closed_set_precision_witness_is_sound(values, external_witness) =>
240 {
241 FactPrecision::Exact
242 }
243 AbstractClassValueV0::FiniteSet { .. } => FactPrecision::Conservative,
244 AbstractClassValueV0::Automaton {
245 automaton,
246 precision_witness,
247 ..
248 } if automaton_precision_witness_is_sound(automaton, precision_witness.as_ref()) => {
249 FactPrecision::Conservative
250 }
251 AbstractClassValueV0::Automaton { .. }
252 | AbstractClassValueV0::Prefix { .. }
253 | AbstractClassValueV0::Suffix { .. }
254 | AbstractClassValueV0::PrefixSuffix { .. }
255 | AbstractClassValueV0::CharInclusion { .. }
256 | AbstractClassValueV0::Composite { .. } => FactPrecision::Heuristic,
257 AbstractClassValueV0::Top { .. } => FactPrecision::Unknown,
258 }
259}
260
261fn automaton_precision_witness_is_sound(
262 automaton: &crate::AbstractStringAutomatonV0,
263 witness: Option<&OmenaAbstractValuePrecisionWitnessV0>,
264) -> bool {
265 matches!(
266 witness,
267 Some(OmenaAbstractValuePrecisionWitnessV0 {
268 direction: OmenaAbstractValueCoverageDirectionV0::SupersetOfProducible,
269 basis: OmenaAbstractValuePrecisionBasisV0::AcyclicExact,
270 authority_digest: None,
271 })
272 ) && automaton_is_well_formed_acyclic(automaton)
273}
274
275fn closed_set_precision_witness_is_sound(
276 values: &[String],
277 witness: Option<&OmenaAbstractValuePrecisionWitnessV0>,
278) -> bool {
279 (2..=MAX_FINITE_CLASS_VALUES).contains(&values.len())
280 && matches!(
281 witness,
282 Some(OmenaAbstractValuePrecisionWitnessV0 {
283 direction: OmenaAbstractValueCoverageDirectionV0::SupersetOfProducible,
284 basis: OmenaAbstractValuePrecisionBasisV0::ClosedSetEnumeration,
285 authority_digest: Some(authority_digest),
286 }) if !authority_digest.is_empty()
287 )
288}
289
290pub(crate) fn normalize_char_set(chars: impl AsRef<str>) -> String {
291 chars
292 .as_ref()
293 .chars()
294 .collect::<BTreeSet<_>>()
295 .into_iter()
296 .collect()
297}
298
299pub(crate) fn union_char_sets(left: &str, right: &str) -> String {
300 normalize_char_set(format!("{left}{right}"))
301}
302
303pub(crate) fn intersect_char_sets(left: &str, right: &str) -> String {
304 let right_set = right.chars().collect::<BTreeSet<_>>();
305 left.chars()
306 .filter(|char| right_set.contains(char))
307 .collect::<BTreeSet<_>>()
308 .into_iter()
309 .collect()
310}
311
312pub(crate) fn char_set_for_string(value: impl AsRef<str>) -> String {
313 normalize_char_set(value)
314}
315
316pub(crate) fn meaningful_longest_common_prefix(values: &[String]) -> String {
317 let prefix = longest_common_prefix(values);
318 if prefix.is_empty() || !is_meaningful_class_prefix(&prefix, values) {
319 return String::new();
320 }
321 prefix
322}
323
324pub(crate) fn meaningful_longest_common_suffix(values: &[String]) -> String {
325 let suffix = longest_common_suffix(values);
326 if suffix.is_empty() || !is_meaningful_class_suffix(&suffix, values) {
327 return String::new();
328 }
329 suffix
330}
331
332pub(crate) fn char_set_is_subset(left: &str, right: &str) -> bool {
333 let right = right.chars().collect::<BTreeSet<_>>();
334 left.chars().all(|char| right.contains(&char))
335}
336
337pub(crate) fn prefix_suffix_min_length(prefix: &str, suffix: &str) -> usize {
338 prefix.len() + suffix.len() - prefix_suffix_overlap_len(prefix, suffix)
339}
340
341pub(crate) fn composite_min_length_for_constraints(
342 prefix: &str,
343 suffix: &str,
344 must_chars: &str,
345) -> usize {
346 let edge_chars = char_set_for_string(format!("{prefix}{suffix}"));
347 let missing_required_char_len = must_chars
348 .chars()
349 .filter(|char| !edge_chars.contains(*char))
350 .map(char::len_utf8)
351 .sum::<usize>();
352
353 if missing_required_char_len == 0 {
354 prefix_suffix_min_length(prefix, suffix)
355 } else {
356 prefix.len() + suffix.len() + missing_required_char_len
357 }
358}
359
360fn prefix_suffix_overlap_len(prefix: &str, suffix: &str) -> usize {
361 let max_overlap = prefix.len().min(suffix.len());
362
363 for overlap in (0..=max_overlap).rev() {
364 let prefix_start = prefix.len() - overlap;
365 if prefix.is_char_boundary(prefix_start)
366 && suffix.is_char_boundary(overlap)
367 && prefix[prefix_start..] == suffix[..overlap]
368 {
369 return overlap;
370 }
371 }
372
373 0
374}
375
376fn normalize_values<I, S>(values: I) -> Vec<String>
377where
378 I: IntoIterator<Item = S>,
379 S: Into<String>,
380{
381 values
382 .into_iter()
383 .map(Into::into)
384 .collect::<BTreeSet<_>>()
385 .into_iter()
386 .collect()
387}
388
389fn longest_common_prefix(values: &[String]) -> String {
390 let Some(first) = values.first() else {
391 return String::new();
392 };
393 let mut prefix = first.clone();
394
395 for value in values.iter().skip(1) {
396 let mut match_length = 0usize;
397 for (left, right) in prefix.chars().zip(value.chars()) {
398 if left != right {
399 break;
400 }
401 match_length += left.len_utf8();
402 }
403 prefix.truncate(match_length);
404 if prefix.is_empty() {
405 break;
406 }
407 }
408
409 prefix
410}
411
412fn longest_common_suffix(values: &[String]) -> String {
413 let reversed = values
414 .iter()
415 .map(|value| value.chars().rev().collect::<String>())
416 .collect::<Vec<_>>();
417 longest_common_prefix(&reversed)
418 .chars()
419 .rev()
420 .collect::<String>()
421}
422
423fn is_meaningful_class_prefix(prefix: &str, values: &[String]) -> bool {
424 if prefix.is_empty() {
425 return false;
426 }
427 if ends_at_class_boundary(prefix) {
428 return true;
429 }
430 values.iter().all(|value| {
431 value.len() == prefix.len()
432 || value[prefix.len()..]
433 .chars()
434 .next()
435 .is_some_and(is_class_boundary_char)
436 })
437}
438
439fn is_meaningful_class_suffix(suffix: &str, values: &[String]) -> bool {
440 if suffix.is_empty() {
441 return false;
442 }
443 if starts_at_class_boundary(suffix) {
444 return true;
445 }
446 values.iter().all(|value| {
447 if value.len() == suffix.len() {
448 return true;
449 }
450 value[..value.len() - suffix.len()]
451 .chars()
452 .next_back()
453 .is_some_and(is_class_boundary_char)
454 })
455}
456
457fn ends_at_class_boundary(value: &str) -> bool {
458 value
459 .chars()
460 .next_back()
461 .is_some_and(is_class_boundary_char)
462}
463
464fn starts_at_class_boundary(value: &str) -> bool {
465 value.chars().next().is_some_and(is_class_boundary_char)
466}
467
468fn is_class_boundary_char(char: char) -> bool {
469 char == '-' || char == '_'
470}