Skip to main content

tldr_cli/commands/contracts/
types.rs

1//! Shared types for Contracts & Flow commands
2//!
3//! This module defines all data types used across the contracts and flow analysis
4//! commands. Types are designed for JSON serialization with serde.
5//!
6//! # Schema Version
7//!
8//! All report types include implicit schema versioning through the module's
9//! SCHEMA_VERSION constant. Consumers should check schema compatibility.
10
11use std::collections::HashMap;
12use std::path::PathBuf;
13
14use clap::ValueEnum;
15use serde::{Deserialize, Serialize};
16
17// =============================================================================
18// Confidence Level
19// =============================================================================
20
21/// Confidence level for inferred contracts and invariants.
22///
23/// Confidence is determined by the source of the inference:
24/// - **High**: Direct code evidence (guard clause, assertion, explicit raise)
25/// - **Medium**: Inferred from patterns or consistent behavior
26/// - **Low**: Derived from type hints or annotations only
27///
28/// # Serialization
29///
30/// Serializes to snake_case: `"high"`, `"medium"`, `"low"`
31#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, Serialize, Deserialize, Default)]
32#[serde(rename_all = "snake_case")]
33pub enum Confidence {
34    /// Direct code evidence (guard clause, assertion)
35    High,
36    /// Inferred from patterns or types
37    #[default]
38    Medium,
39    /// Derived from type hints only
40    Low,
41}
42
43impl std::fmt::Display for Confidence {
44    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
45        match self {
46            Self::High => write!(f, "high"),
47            Self::Medium => write!(f, "medium"),
48            Self::Low => write!(f, "low"),
49        }
50    }
51}
52
53// =============================================================================
54// Condition (Contract Element)
55// =============================================================================
56
57/// A single contract condition (precondition, postcondition, or invariant).
58///
59/// Represents a constraint on a variable that was detected in the source code.
60///
61/// # Example
62///
63/// ```json
64/// {
65///   "variable": "x",
66///   "constraint": "x >= 0",
67///   "source_line": 10,
68///   "confidence": "high"
69/// }
70/// ```
71#[derive(Debug, Clone, PartialEq, Serialize, Deserialize)]
72pub struct Condition {
73    /// Variable name this condition applies to
74    pub variable: String,
75
76    /// Human-readable constraint expression (e.g., "x > 0", "isinstance(x, str)")
77    pub constraint: String,
78
79    /// Source line where condition was detected (1-indexed)
80    pub source_line: u32,
81
82    /// Confidence level of this condition
83    pub confidence: Confidence,
84}
85
86impl Condition {
87    /// Create a new condition with High confidence (from guard clause/assert)
88    pub fn high(variable: impl Into<String>, constraint: impl Into<String>, line: u32) -> Self {
89        Self {
90            variable: variable.into(),
91            constraint: constraint.into(),
92            source_line: line,
93            confidence: Confidence::High,
94        }
95    }
96
97    /// Create a new condition with Medium confidence (from patterns)
98    pub fn medium(variable: impl Into<String>, constraint: impl Into<String>, line: u32) -> Self {
99        Self {
100            variable: variable.into(),
101            constraint: constraint.into(),
102            source_line: line,
103            confidence: Confidence::Medium,
104        }
105    }
106
107    /// Create a new condition with Low confidence (from type hints)
108    pub fn low(variable: impl Into<String>, constraint: impl Into<String>, line: u32) -> Self {
109        Self {
110            variable: variable.into(),
111            constraint: constraint.into(),
112            source_line: line,
113            confidence: Confidence::Low,
114        }
115    }
116}
117
118// =============================================================================
119// Invariant Types
120// =============================================================================
121
122/// Types of invariants that can be inferred from test traces.
123///
124/// Based on Daikon-style invariant templates.
125///
126/// # Serialization
127///
128/// Serializes to snake_case: `"type"`, `"non_null"`, `"non_negative"`, etc.
129#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, Serialize, Deserialize)]
130#[serde(rename_all = "snake_case")]
131pub enum InvariantKind {
132    /// Type invariant (e.g., "x: int")
133    Type,
134    /// Non-null invariant (no None values observed)
135    NonNull,
136    /// Non-negative numeric (all values >= 0)
137    NonNegative,
138    /// Positive numeric (all values > 0)
139    Positive,
140    /// Range constraint (min <= x <= max)
141    Range,
142    /// Ordering relation between parameters (e.g., start < end)
143    Relation,
144    /// Length constraint (e.g., len(x) > 0)
145    Length,
146}
147
148impl std::fmt::Display for InvariantKind {
149    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
150        match self {
151            Self::Type => write!(f, "type"),
152            Self::NonNull => write!(f, "non_null"),
153            Self::NonNegative => write!(f, "non_negative"),
154            Self::Positive => write!(f, "positive"),
155            Self::Range => write!(f, "range"),
156            Self::Relation => write!(f, "relation"),
157            Self::Length => write!(f, "length"),
158        }
159    }
160}
161
162/// An inferred invariant from test execution traces.
163///
164/// Invariants are derived from observing function behavior across multiple
165/// test executions.
166#[derive(Debug, Clone, PartialEq, Serialize, Deserialize)]
167pub struct Invariant {
168    /// Variable name this invariant applies to
169    pub variable: String,
170
171    /// Kind of invariant
172    pub kind: InvariantKind,
173
174    /// Human-readable expression (e.g., "x >= 0", "isinstance(x, int)")
175    pub expression: String,
176
177    /// Confidence level based on observation count
178    pub confidence: Confidence,
179
180    /// Number of observations supporting this invariant
181    pub observations: u32,
182
183    /// Number of counterexamples observed (should be 0 for valid invariants)
184    pub counterexample_count: u32,
185}
186
187// =============================================================================
188// Spec Types (from test extraction)
189// =============================================================================
190
191/// Input/Output specification from a test assertion.
192///
193/// Extracted from patterns like `assert func(args) == expected`.
194#[derive(Debug, Clone, PartialEq, Serialize, Deserialize)]
195pub struct InputOutputSpec {
196    /// Function being tested
197    pub function: String,
198
199    /// Input arguments (as JSON values)
200    pub inputs: Vec<serde_json::Value>,
201
202    /// Expected output (as JSON value)
203    pub output: serde_json::Value,
204
205    /// Name of the test function where this was found
206    pub test_function: String,
207
208    /// Line number in the test file
209    pub line: u32,
210
211    /// Confidence level
212    pub confidence: Confidence,
213}
214
215/// Exception specification from pytest.raises.
216///
217/// Extracted from patterns like `with pytest.raises(ValueError)`.
218#[derive(Debug, Clone, PartialEq, Serialize, Deserialize)]
219pub struct ExceptionSpec {
220    /// Function being tested
221    pub function: String,
222
223    /// Input arguments that trigger the exception
224    pub inputs: Vec<serde_json::Value>,
225
226    /// Exception type expected (e.g., "ValueError")
227    pub exception_type: String,
228
229    /// Optional match pattern for exception message
230    pub match_pattern: Option<String>,
231
232    /// Name of the test function where this was found
233    pub test_function: String,
234
235    /// Line number in the test file
236    pub line: u32,
237
238    /// Confidence level
239    pub confidence: Confidence,
240}
241
242/// Property specification from test assertions.
243///
244/// Extracted from patterns like `assert isinstance(f(x), T)` or `assert len(f(x)) == n`.
245#[derive(Debug, Clone, PartialEq, Serialize, Deserialize)]
246pub struct PropertySpec {
247    /// Function being tested
248    pub function: String,
249
250    /// Type of property: "type", "length", "bounds", "boolean", "membership", "not_none"
251    pub property_type: String,
252
253    /// Human-readable constraint
254    pub constraint: String,
255
256    /// Name of the test function where this was found
257    pub test_function: String,
258
259    /// Line number in the test file
260    pub line: u32,
261
262    /// Confidence level
263    pub confidence: Confidence,
264}
265
266// =============================================================================
267// Interval (for bounds analysis)
268// =============================================================================
269
270/// Numeric interval [lo, hi] for bounds analysis.
271///
272/// Represents the range of possible values for a numeric variable.
273/// Uses f64 for flexibility (handles both int and float).
274///
275/// # Special Values
276///
277/// - `top()`: [NEG_INFINITY, INFINITY] - any value possible
278/// - `bottom()`: [INFINITY, NEG_INFINITY] - no valid values (unreachable)
279/// - `const_val(n)`: [n, n] - exactly one value
280#[derive(Debug, Clone, Copy, PartialEq)]
281pub struct Interval {
282    /// Lower bound (f64::NEG_INFINITY for unbounded below)
283    pub lo: f64,
284
285    /// Upper bound (f64::INFINITY for unbounded above)
286    pub hi: f64,
287}
288
289// Custom serialization to handle infinity values as strings
290impl Serialize for Interval {
291    fn serialize<S>(&self, serializer: S) -> Result<S::Ok, S::Error>
292    where
293        S: serde::Serializer,
294    {
295        use serde::ser::SerializeStruct;
296        let mut state = serializer.serialize_struct("Interval", 2)?;
297
298        // Serialize lo
299        if self.lo == f64::NEG_INFINITY {
300            state.serialize_field("lo", "-inf")?;
301        } else if self.lo == f64::INFINITY {
302            state.serialize_field("lo", "+inf")?;
303        } else if self.lo.is_nan() {
304            state.serialize_field("lo", "NaN")?;
305        } else {
306            state.serialize_field("lo", &self.lo)?;
307        }
308
309        // Serialize hi
310        if self.hi == f64::NEG_INFINITY {
311            state.serialize_field("hi", "-inf")?;
312        } else if self.hi == f64::INFINITY {
313            state.serialize_field("hi", "+inf")?;
314        } else if self.hi.is_nan() {
315            state.serialize_field("hi", "NaN")?;
316        } else {
317            state.serialize_field("hi", &self.hi)?;
318        }
319
320        state.end()
321    }
322}
323
324// Custom deserialization to handle infinity values as strings
325impl<'de> Deserialize<'de> for Interval {
326    fn deserialize<D>(deserializer: D) -> Result<Self, D::Error>
327    where
328        D: serde::Deserializer<'de>,
329    {
330        #[derive(Deserialize)]
331        struct IntervalHelper {
332            lo: serde_json::Value,
333            hi: serde_json::Value,
334        }
335
336        let helper = IntervalHelper::deserialize(deserializer)?;
337
338        fn parse_bound(v: serde_json::Value) -> Result<f64, String> {
339            match v {
340                serde_json::Value::Number(n) => {
341                    n.as_f64().ok_or_else(|| "invalid number".to_string())
342                }
343                serde_json::Value::String(s) => match s.as_str() {
344                    "-inf" | "-Infinity" => Ok(f64::NEG_INFINITY),
345                    "+inf" | "inf" | "Infinity" => Ok(f64::INFINITY),
346                    "NaN" => Ok(f64::NAN),
347                    _ => s.parse::<f64>().map_err(|e| e.to_string()),
348                },
349                serde_json::Value::Null => Ok(f64::INFINITY), // null defaults to infinity
350                _ => Err("expected number or string".to_string()),
351            }
352        }
353
354        let lo = parse_bound(helper.lo).map_err(serde::de::Error::custom)?;
355        let hi = parse_bound(helper.hi).map_err(serde::de::Error::custom)?;
356
357        Ok(Interval { lo, hi })
358    }
359}
360
361impl Interval {
362    /// Create an interval containing exactly one value.
363    pub fn const_val(n: f64) -> Self {
364        Self { lo: n, hi: n }
365    }
366
367    /// Create the top element (any value possible).
368    pub fn top() -> Self {
369        Self {
370            lo: f64::NEG_INFINITY,
371            hi: f64::INFINITY,
372        }
373    }
374
375    /// Create the bottom element (no valid values - unreachable).
376    pub fn bottom() -> Self {
377        Self {
378            lo: f64::INFINITY,
379            hi: f64::NEG_INFINITY,
380        }
381    }
382
383    /// Check if this interval is bottom (empty/unreachable).
384    pub fn is_bottom(&self) -> bool {
385        self.lo > self.hi
386    }
387
388    /// Check if this interval is top (any value possible).
389    pub fn is_top(&self) -> bool {
390        self.lo == f64::NEG_INFINITY && self.hi == f64::INFINITY
391    }
392
393    /// Check if this interval contains a specific value.
394    pub fn contains(&self, n: f64) -> bool {
395        !self.is_bottom() && self.lo <= n && n <= self.hi
396    }
397
398    /// Check if this interval contains zero (important for division-by-zero detection).
399    pub fn contains_zero(&self) -> bool {
400        self.contains(0.0)
401    }
402
403    /// Compute the join (least upper bound) of two intervals.
404    ///
405    /// `[a,b] | [c,d] = [min(a,c), max(b,d)]`
406    pub fn join(&self, other: &Self) -> Self {
407        if self.is_bottom() {
408            return *other;
409        }
410        if other.is_bottom() {
411            return *self;
412        }
413        Self {
414            lo: self.lo.min(other.lo),
415            hi: self.hi.max(other.hi),
416        }
417    }
418
419    /// Compute the meet (greatest lower bound) of two intervals.
420    ///
421    /// `[a,b] & [c,d] = [max(a,c), min(b,d)]` or bottom if empty
422    pub fn meet(&self, other: &Self) -> Self {
423        if self.is_bottom() || other.is_bottom() {
424            return Self::bottom();
425        }
426        // Result may be bottom if intervals don't overlap.
427        Self {
428            lo: self.lo.max(other.lo),
429            hi: self.hi.min(other.hi),
430        }
431    }
432
433    /// Widen this interval based on new observations.
434    ///
435    /// Used to ensure convergence in fixpoint iteration.
436    /// `[a,b] W [c,d] = [c<a ? -inf : a, d>b ? +inf : b]`
437    pub fn widen(&self, other: &Self) -> Self {
438        if self.is_bottom() {
439            return *other;
440        }
441        if other.is_bottom() {
442            return *self;
443        }
444        Self {
445            lo: if other.lo < self.lo {
446                f64::NEG_INFINITY
447            } else {
448                self.lo
449            },
450            hi: if other.hi > self.hi {
451                f64::INFINITY
452            } else {
453                self.hi
454            },
455        }
456    }
457
458    /// Add two intervals: [a,b] + [c,d] = [a+c, b+d]
459    pub fn add(&self, other: &Self) -> Self {
460        if self.is_bottom() || other.is_bottom() {
461            return Self::bottom();
462        }
463        Self {
464            lo: self.lo + other.lo,
465            hi: self.hi + other.hi,
466        }
467    }
468
469    /// Subtract two intervals: [a,b] - [c,d] = [a-d, b-c]
470    pub fn sub(&self, other: &Self) -> Self {
471        if self.is_bottom() || other.is_bottom() {
472            return Self::bottom();
473        }
474        Self {
475            lo: self.lo - other.hi,
476            hi: self.hi - other.lo,
477        }
478    }
479
480    /// Multiply two intervals.
481    ///
482    /// Handles sign combinations correctly.
483    pub fn mul(&self, other: &Self) -> Self {
484        if self.is_bottom() || other.is_bottom() {
485            return Self::bottom();
486        }
487        // Compute all four products and take min/max
488        let products = [
489            self.lo * other.lo,
490            self.lo * other.hi,
491            self.hi * other.lo,
492            self.hi * other.hi,
493        ];
494        Self {
495            lo: products.iter().cloned().fold(f64::INFINITY, f64::min),
496            hi: products.iter().cloned().fold(f64::NEG_INFINITY, f64::max),
497        }
498    }
499
500    /// Divide two intervals.
501    ///
502    /// Returns (result, may_divide_by_zero) where may_divide_by_zero is true
503    /// if the divisor interval contains zero.
504    pub fn div(&self, other: &Self) -> (Self, bool) {
505        if self.is_bottom() || other.is_bottom() {
506            return (Self::bottom(), false);
507        }
508
509        let may_div_zero = other.contains_zero();
510
511        // If divisor is exactly [0,0], result is bottom (undefined)
512        if other.lo == 0.0 && other.hi == 0.0 {
513            return (Self::bottom(), true);
514        }
515
516        // Handle cases where divisor contains zero
517        if may_div_zero {
518            // Conservative: return top
519            return (Self::top(), true);
520        }
521
522        // Safe division: divisor doesn't contain zero
523        let products = [
524            self.lo / other.lo,
525            self.lo / other.hi,
526            self.hi / other.lo,
527            self.hi / other.hi,
528        ];
529        (
530            Self {
531                lo: products.iter().cloned().fold(f64::INFINITY, f64::min),
532                hi: products.iter().cloned().fold(f64::NEG_INFINITY, f64::max),
533            },
534            false,
535        )
536    }
537
538    /// Negate an interval: -[a,b] = [-b, -a]
539    pub fn neg(&self) -> Self {
540        if self.is_bottom() {
541            return Self::bottom();
542        }
543        Self {
544            lo: -self.hi,
545            hi: -self.lo,
546        }
547    }
548}
549
550impl Default for Interval {
551    fn default() -> Self {
552        Self::top()
553    }
554}
555
556impl std::fmt::Display for Interval {
557    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
558        if self.is_bottom() {
559            write!(f, "bottom")
560        } else if self.is_top() {
561            write!(f, "(-inf, +inf)")
562        } else if self.lo == self.hi {
563            write!(f, "[{}]", self.lo)
564        } else {
565            let lo_str = if self.lo == f64::NEG_INFINITY {
566                "-inf".to_string()
567            } else {
568                self.lo.to_string()
569            };
570            let hi_str = if self.hi == f64::INFINITY {
571                "+inf".to_string()
572            } else {
573                self.hi.to_string()
574            };
575            write!(f, "[{}, {}]", lo_str, hi_str)
576        }
577    }
578}
579
580// =============================================================================
581// Dead Store Detection
582// =============================================================================
583
584/// A dead store detected in SSA form.
585///
586/// A definition is dead if it has no uses (empty use_sites).
587#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
588pub struct DeadStore {
589    /// Original variable name (without SSA version suffix)
590    pub variable: String,
591
592    /// SSA versioned name (e.g., "x_2")
593    pub ssa_name: String,
594
595    /// Line number of the dead assignment (1-indexed)
596    pub line: u32,
597
598    /// Block ID where assignment occurs
599    pub block_id: u32,
600
601    /// Whether this is a phi function definition
602    pub is_phi: bool,
603}
604
605impl DeadStore {
606    /// Convert to JSON value for compatibility with spec
607    pub fn to_dict(&self) -> serde_json::Value {
608        serde_json::json!({
609            "variable": self.variable,
610            "ssa_name": self.ssa_name,
611            "line": self.line,
612            "block_id": self.block_id,
613            "is_phi": self.is_phi,
614        })
615    }
616}
617
618// =============================================================================
619// Chop Result (Slice Intersection)
620// =============================================================================
621
622/// Result of a chop operation (slice intersection).
623///
624/// Chop computes `forward_slice(source) AND backward_slice(target)` to find
625/// all statements on any path from source to target.
626#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
627pub struct ChopResult {
628    /// Lines on the dependency path (sorted)
629    pub lines: Vec<u32>,
630
631    /// Number of lines on the path
632    pub count: u32,
633
634    /// Source line (where data flows FROM)
635    pub source_line: u32,
636
637    /// Target line (where data flows TO)
638    pub target_line: u32,
639
640    /// True if source_line is in backward_slice(target_line)
641    pub path_exists: bool,
642
643    /// Function name containing the analysis
644    pub function: String,
645
646    /// Human-readable explanation of the result
647    pub explanation: Option<String>,
648}
649
650impl ChopResult {
651    /// Create a result for when source and target are the same line.
652    pub fn same_line(line: u32, function: impl Into<String>) -> Self {
653        Self {
654            lines: vec![line],
655            count: 1,
656            source_line: line,
657            target_line: line,
658            path_exists: true,
659            function: function.into(),
660            explanation: Some(format!("Source and target are the same line ({}).", line)),
661        }
662    }
663
664    /// Create a result for when no path exists.
665    pub fn no_path(source: u32, target: u32, function: impl Into<String>) -> Self {
666        Self {
667            lines: vec![],
668            count: 0,
669            source_line: source,
670            target_line: target,
671            path_exists: false,
672            function: function.into(),
673            explanation: Some(format!(
674                "No dependency path from line {} to line {}. \
675                 The source line does not affect the target line.",
676                source, target
677            )),
678        }
679    }
680}
681
682// =============================================================================
683// Interval Warning
684// =============================================================================
685
686/// Warning from interval/bounds analysis.
687///
688/// Generated when analysis detects potential runtime issues like division by zero.
689#[derive(Debug, Clone, PartialEq, Serialize, Deserialize)]
690pub struct IntervalWarning {
691    /// Line number where the warning applies
692    pub line: u32,
693
694    /// Kind of warning: "division_by_zero", "out_of_bounds", "overflow"
695    pub kind: String,
696
697    /// Variable involved
698    pub variable: String,
699
700    /// Current bounds for the variable
701    pub bounds: Interval,
702
703    /// Human-readable warning message
704    pub message: String,
705}
706
707// =============================================================================
708// Report Types
709// =============================================================================
710
711/// Report from the contracts command.
712#[derive(Debug, Clone, PartialEq, Serialize, Deserialize)]
713pub struct ContractsReport {
714    /// Function analyzed
715    pub function: String,
716
717    /// File path
718    pub file: PathBuf,
719
720    /// Detected preconditions
721    pub preconditions: Vec<Condition>,
722
723    /// Detected postconditions
724    pub postconditions: Vec<Condition>,
725
726    /// Detected invariants
727    pub invariants: Vec<Condition>,
728}
729
730/// Invariants for a single function.
731#[derive(Debug, Clone, PartialEq, Serialize, Deserialize)]
732pub struct FunctionInvariants {
733    /// Function name
734    pub function_name: String,
735
736    /// Inferred preconditions
737    pub preconditions: Vec<Invariant>,
738
739    /// Inferred postconditions
740    pub postconditions: Vec<Invariant>,
741
742    /// Total observations used for inference
743    pub observation_count: u32,
744}
745
746/// Summary of invariant inference.
747#[derive(Debug, Clone, PartialEq, Serialize, Deserialize)]
748pub struct InvariantsSummary {
749    /// Total test observations across all functions
750    pub total_observations: u32,
751
752    /// Total invariants inferred
753    pub total_invariants: u32,
754
755    /// Count by invariant kind
756    pub by_kind: HashMap<String, u32>,
757}
758
759/// Full report from the invariants command.
760#[derive(Debug, Clone, PartialEq, Serialize, Deserialize)]
761pub struct InvariantsReport {
762    /// Invariants by function
763    pub functions: Vec<FunctionInvariants>,
764
765    /// Summary statistics
766    pub summary: InvariantsSummary,
767}
768
769/// Specs for a single function.
770#[derive(Debug, Clone, PartialEq, Serialize, Deserialize)]
771pub struct FunctionSpecs {
772    /// Function name
773    pub function_name: String,
774
775    /// Human-readable summary (e.g., "3 input/output, 1 raises")
776    pub summary: String,
777
778    /// Number of test functions that test this function
779    pub test_count: u32,
780
781    /// Input/output specifications
782    pub input_output_specs: Vec<InputOutputSpec>,
783
784    /// Exception specifications
785    pub exception_specs: Vec<ExceptionSpec>,
786
787    /// Property specifications
788    pub property_specs: Vec<PropertySpec>,
789}
790
791/// Counts by spec type.
792#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
793pub struct SpecsByType {
794    /// Input/output spec count
795    pub input_output: u32,
796
797    /// Exception spec count
798    pub exception: u32,
799
800    /// Property spec count
801    pub property: u32,
802}
803
804/// Summary of specs extraction.
805#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
806pub struct SpecsSummary {
807    /// Total specs extracted
808    pub total_specs: u32,
809
810    /// Counts by type
811    pub by_type: SpecsByType,
812
813    /// Number of test functions scanned
814    pub test_functions_scanned: u32,
815
816    /// Number of test files scanned
817    pub test_files_scanned: u32,
818
819    /// Number of unique functions found
820    pub functions_found: u32,
821}
822
823/// Full report from the specs command.
824#[derive(Debug, Clone, PartialEq, Serialize, Deserialize)]
825pub struct SpecsReport {
826    /// Specs by function
827    pub functions: Vec<FunctionSpecs>,
828
829    /// Summary statistics
830    pub summary: SpecsSummary,
831}
832
833/// Result from the bounds command.
834#[derive(Debug, Clone, PartialEq, Serialize, Deserialize)]
835pub struct BoundsResult {
836    /// Function analyzed
837    pub function: String,
838
839    /// Interval bounds: line -> variable -> interval
840    pub bounds: HashMap<u32, HashMap<String, Interval>>,
841
842    /// Warnings (e.g., potential division by zero)
843    pub warnings: Vec<IntervalWarning>,
844
845    /// Whether analysis converged
846    pub converged: bool,
847
848    /// Number of fixpoint iterations
849    pub iterations: u32,
850}
851
852/// Report from the dead-stores command.
853#[derive(Debug, Clone, PartialEq, Serialize, Deserialize)]
854pub struct DeadStoresReport {
855    /// Function analyzed
856    pub function: String,
857
858    /// File path
859    pub file: PathBuf,
860
861    /// Dead stores detected via SSA analysis
862    pub dead_stores_ssa: Vec<DeadStore>,
863
864    /// Count of dead stores
865    pub count: u32,
866
867    /// Optional: dead stores via live-vars analysis (if --compare flag used)
868    pub dead_stores_live_vars: Option<Vec<DeadStore>>,
869
870    /// Optional: count from live-vars analysis
871    pub live_vars_count: Option<u32>,
872}
873
874/// Status of a sub-analysis in verify command.
875#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize, Deserialize)]
876#[serde(rename_all = "snake_case")]
877pub enum SubAnalysisStatus {
878    /// Analysis completed successfully
879    Success,
880    /// Analysis completed with partial results (some files failed)
881    Partial,
882    /// Analysis failed completely
883    Failed,
884    /// Analysis was skipped (e.g., in quick mode)
885    Skipped,
886}
887
888impl SubAnalysisStatus {
889    /// Returns true if the analysis succeeded (fully or partially)
890    pub fn is_success(&self) -> bool {
891        matches!(self, Self::Success | Self::Partial)
892    }
893}
894
895/// Result from a sub-analysis in verify command.
896#[derive(Debug, Clone, PartialEq, Serialize, Deserialize)]
897pub struct SubAnalysisResult {
898    /// Name of the sub-analysis
899    pub name: String,
900
901    /// Status of the analysis
902    pub status: SubAnalysisStatus,
903
904    /// Number of items found (contracts, specs, warnings, etc.)
905    pub items_found: u32,
906
907    /// Time taken in milliseconds
908    pub elapsed_ms: u64,
909
910    /// Error message if failed or partial
911    pub error: Option<String>,
912
913    /// Analysis data (command-specific)
914    pub data: Option<serde_json::Value>,
915}
916
917impl SubAnalysisResult {
918    /// Returns true if the analysis succeeded (for backward compatibility)
919    pub fn success(&self) -> bool {
920        self.status.is_success()
921    }
922}
923
924/// Coverage information from verify command.
925#[derive(Debug, Clone, PartialEq, Serialize, Deserialize)]
926pub struct CoverageInfo {
927    /// Number of functions with at least one constraint
928    pub constrained_functions: u32,
929
930    /// Total functions analyzed
931    pub total_functions: u32,
932
933    /// Coverage percentage (0.0 - 100.0)
934    pub coverage_pct: f64,
935}
936
937/// Summary from verify command.
938#[derive(Debug, Clone, PartialEq, Serialize, Deserialize)]
939pub struct VerifySummary {
940    /// Specs extracted from tests
941    pub spec_count: u32,
942
943    /// Invariants inferred
944    pub invariant_count: u32,
945
946    /// Contracts inferred
947    pub contract_count: u32,
948
949    /// Annotated[T] constraints found
950    pub annotated_count: u32,
951
952    /// Behavioral models extracted
953    pub behavioral_count: u32,
954
955    /// Patterns detected
956    pub pattern_count: u32,
957
958    /// High-confidence patterns
959    pub pattern_high_confidence: u32,
960
961    /// Function coverage information
962    pub coverage: CoverageInfo,
963}
964
965/// Full report from verify command.
966#[derive(Debug, Clone, PartialEq, Serialize, Deserialize)]
967pub struct VerifyReport {
968    /// Path analyzed
969    pub path: PathBuf,
970
971    /// Results from each sub-analysis
972    pub sub_results: HashMap<String, SubAnalysisResult>,
973
974    /// Summary statistics
975    pub summary: VerifySummary,
976
977    /// Total time taken in milliseconds
978    pub total_elapsed_ms: u64,
979
980    /// Number of files analyzed
981    pub files_analyzed: u32,
982
983    /// Number of files that failed to analyze
984    pub files_failed: u32,
985
986    /// Whether some results are partial (some files or analyses failed)
987    pub partial_results: bool,
988}
989
990// =============================================================================
991// Output Format
992// =============================================================================
993
994/// Output format for command results.
995#[derive(Debug, Clone, Copy, PartialEq, Eq, Default, ValueEnum)]
996pub enum OutputFormat {
997    /// JSON output (default)
998    #[default]
999    Json,
1000
1001    /// Human-readable text output
1002    Text,
1003}
1004
1005impl std::fmt::Display for OutputFormat {
1006    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
1007        match self {
1008            Self::Json => write!(f, "json"),
1009            Self::Text => write!(f, "text"),
1010        }
1011    }
1012}
1013
1014// =============================================================================
1015// Tests
1016// =============================================================================
1017
1018#[cfg(test)]
1019mod tests {
1020    use super::*;
1021
1022    // -------------------------------------------------------------------------
1023    // Confidence Tests
1024    // -------------------------------------------------------------------------
1025
1026    #[test]
1027    fn test_confidence_enum_serialization() {
1028        assert_eq!(
1029            serde_json::to_string(&Confidence::High).unwrap(),
1030            "\"high\""
1031        );
1032        assert_eq!(
1033            serde_json::to_string(&Confidence::Medium).unwrap(),
1034            "\"medium\""
1035        );
1036        assert_eq!(serde_json::to_string(&Confidence::Low).unwrap(), "\"low\"");
1037    }
1038
1039    #[test]
1040    fn test_confidence_enum_deserialization() {
1041        assert_eq!(
1042            serde_json::from_str::<Confidence>("\"high\"").unwrap(),
1043            Confidence::High
1044        );
1045        assert_eq!(
1046            serde_json::from_str::<Confidence>("\"medium\"").unwrap(),
1047            Confidence::Medium
1048        );
1049        assert_eq!(
1050            serde_json::from_str::<Confidence>("\"low\"").unwrap(),
1051            Confidence::Low
1052        );
1053    }
1054
1055    #[test]
1056    fn test_confidence_default() {
1057        assert_eq!(Confidence::default(), Confidence::Medium);
1058    }
1059
1060    // -------------------------------------------------------------------------
1061    // Condition Tests
1062    // -------------------------------------------------------------------------
1063
1064    #[test]
1065    fn test_condition_struct_fields() {
1066        let cond = Condition::high("x", "x >= 0", 10);
1067        assert_eq!(cond.variable, "x");
1068        assert_eq!(cond.constraint, "x >= 0");
1069        assert_eq!(cond.source_line, 10);
1070        assert_eq!(cond.confidence, Confidence::High);
1071    }
1072
1073    #[test]
1074    fn test_condition_serialization() {
1075        let cond = Condition::high("x", "x >= 0", 10);
1076        let json = serde_json::to_string(&cond).unwrap();
1077        assert!(json.contains("\"variable\":\"x\""));
1078        assert!(json.contains("\"confidence\":\"high\""));
1079    }
1080
1081    // -------------------------------------------------------------------------
1082    // Interval Tests
1083    // -------------------------------------------------------------------------
1084
1085    #[test]
1086    fn test_interval_const_val() {
1087        let i = Interval::const_val(5.0);
1088        assert_eq!(i.lo, 5.0);
1089        assert_eq!(i.hi, 5.0);
1090        assert!(i.contains(5.0));
1091        assert!(!i.contains(4.0));
1092        assert!(!i.contains(6.0));
1093    }
1094
1095    #[test]
1096    fn test_interval_basic_operations() {
1097        let i = Interval { lo: 0.0, hi: 10.0 };
1098        assert!(i.contains(0.0));
1099        assert!(i.contains(5.0));
1100        assert!(i.contains(10.0));
1101        assert!(!i.contains(-1.0));
1102        assert!(!i.contains(11.0));
1103    }
1104
1105    #[test]
1106    fn test_interval_bottom_top_detection() {
1107        assert!(Interval::bottom().is_bottom());
1108        assert!(!Interval::top().is_bottom());
1109        assert!(Interval::top().is_top());
1110        assert!(!Interval::bottom().is_top());
1111        assert!(!Interval::const_val(5.0).is_bottom());
1112        assert!(!Interval::const_val(5.0).is_top());
1113    }
1114
1115    #[test]
1116    fn test_interval_contains_zero() {
1117        assert!(Interval { lo: -5.0, hi: 5.0 }.contains_zero());
1118        assert!(Interval { lo: 0.0, hi: 10.0 }.contains_zero());
1119        assert!(Interval { lo: -10.0, hi: 0.0 }.contains_zero());
1120        assert!(!Interval { lo: 1.0, hi: 10.0 }.contains_zero());
1121        assert!(!Interval {
1122            lo: -10.0,
1123            hi: -1.0
1124        }
1125        .contains_zero());
1126    }
1127
1128    #[test]
1129    fn test_interval_join() {
1130        let a = Interval { lo: 0.0, hi: 5.0 };
1131        let b = Interval { lo: 3.0, hi: 10.0 };
1132        let joined = a.join(&b);
1133        assert_eq!(joined.lo, 0.0);
1134        assert_eq!(joined.hi, 10.0);
1135    }
1136
1137    #[test]
1138    fn test_interval_meet() {
1139        let a = Interval { lo: 0.0, hi: 5.0 };
1140        let b = Interval { lo: 3.0, hi: 10.0 };
1141        let met = a.meet(&b);
1142        assert_eq!(met.lo, 3.0);
1143        assert_eq!(met.hi, 5.0);
1144    }
1145
1146    #[test]
1147    fn test_interval_add() {
1148        let a = Interval { lo: 1.0, hi: 5.0 };
1149        let b = Interval { lo: 2.0, hi: 3.0 };
1150        let sum = a.add(&b);
1151        assert_eq!(sum.lo, 3.0);
1152        assert_eq!(sum.hi, 8.0);
1153    }
1154
1155    #[test]
1156    fn test_interval_sub() {
1157        let a = Interval { lo: 5.0, hi: 10.0 };
1158        let b = Interval { lo: 1.0, hi: 3.0 };
1159        let diff = a.sub(&b);
1160        assert_eq!(diff.lo, 2.0); // 5 - 3
1161        assert_eq!(diff.hi, 9.0); // 10 - 1
1162    }
1163
1164    #[test]
1165    fn test_interval_mul() {
1166        let a = Interval { lo: 2.0, hi: 3.0 };
1167        let b = Interval { lo: 4.0, hi: 5.0 };
1168        let prod = a.mul(&b);
1169        assert_eq!(prod.lo, 8.0);
1170        assert_eq!(prod.hi, 15.0);
1171    }
1172
1173    #[test]
1174    fn test_interval_mul_negative() {
1175        let a = Interval { lo: -2.0, hi: 3.0 };
1176        let b = Interval { lo: -1.0, hi: 2.0 };
1177        let prod = a.mul(&b);
1178        // Products: 2, -4, -3, 6 -> min=-4, max=6
1179        assert_eq!(prod.lo, -4.0);
1180        assert_eq!(prod.hi, 6.0);
1181    }
1182
1183    #[test]
1184    fn test_interval_div() {
1185        let a = Interval { lo: 10.0, hi: 20.0 };
1186        let b = Interval { lo: 2.0, hi: 5.0 };
1187        let (quot, div_zero) = a.div(&b);
1188        assert!(!div_zero);
1189        assert_eq!(quot.lo, 2.0); // 10 / 5
1190        assert_eq!(quot.hi, 10.0); // 20 / 2
1191    }
1192
1193    #[test]
1194    fn test_interval_div_by_zero() {
1195        let a = Interval { lo: 10.0, hi: 20.0 };
1196        let b = Interval { lo: -1.0, hi: 1.0 }; // Contains zero
1197        let (_, div_zero) = a.div(&b);
1198        assert!(div_zero);
1199    }
1200
1201    #[test]
1202    fn test_interval_widen() {
1203        let a = Interval { lo: 0.0, hi: 10.0 };
1204        let b = Interval { lo: -5.0, hi: 15.0 };
1205        let widened = a.widen(&b);
1206        assert_eq!(widened.lo, f64::NEG_INFINITY);
1207        assert_eq!(widened.hi, f64::INFINITY);
1208    }
1209
1210    // -------------------------------------------------------------------------
1211    // Dead Store Tests
1212    // -------------------------------------------------------------------------
1213
1214    #[test]
1215    fn test_dead_store_struct() {
1216        let ds = DeadStore {
1217            variable: "x".to_string(),
1218            ssa_name: "x_2".to_string(),
1219            line: 10,
1220            block_id: 1,
1221            is_phi: false,
1222        };
1223        assert_eq!(ds.variable, "x");
1224        assert_eq!(ds.ssa_name, "x_2");
1225        assert_eq!(ds.line, 10);
1226        assert!(!ds.is_phi);
1227    }
1228
1229    #[test]
1230    fn test_dead_store_serialization() {
1231        let ds = DeadStore {
1232            variable: "x".to_string(),
1233            ssa_name: "x_2".to_string(),
1234            line: 10,
1235            block_id: 1,
1236            is_phi: false,
1237        };
1238        let json = serde_json::to_string(&ds).unwrap();
1239        assert!(json.contains("\"variable\":\"x\""));
1240        assert!(json.contains("\"ssa_name\":\"x_2\""));
1241    }
1242
1243    // -------------------------------------------------------------------------
1244    // Chop Result Tests
1245    // -------------------------------------------------------------------------
1246
1247    #[test]
1248    fn test_chop_result_struct() {
1249        let result = ChopResult {
1250            lines: vec![2, 3, 4],
1251            count: 3,
1252            source_line: 2,
1253            target_line: 4,
1254            path_exists: true,
1255            function: "example".to_string(),
1256            explanation: Some("Found path".to_string()),
1257        };
1258        assert_eq!(result.count, 3);
1259        assert!(result.path_exists);
1260    }
1261
1262    #[test]
1263    fn test_chop_result_same_line() {
1264        let result = ChopResult::same_line(5, "test_func");
1265        assert_eq!(result.lines, vec![5]);
1266        assert_eq!(result.count, 1);
1267        assert!(result.path_exists);
1268    }
1269
1270    #[test]
1271    fn test_chop_result_no_path() {
1272        let result = ChopResult::no_path(2, 10, "test_func");
1273        assert!(result.lines.is_empty());
1274        assert_eq!(result.count, 0);
1275        assert!(!result.path_exists);
1276    }
1277
1278    // -------------------------------------------------------------------------
1279    // Contracts Report Tests
1280    // -------------------------------------------------------------------------
1281
1282    #[test]
1283    fn test_contracts_report_struct() {
1284        let report = ContractsReport {
1285            function: "process_data".to_string(),
1286            file: PathBuf::from("test.py"),
1287            preconditions: vec![Condition::high("x", "x >= 0", 10)],
1288            postconditions: vec![],
1289            invariants: vec![],
1290        };
1291        assert_eq!(report.function, "process_data");
1292        assert_eq!(report.preconditions.len(), 1);
1293    }
1294
1295    // -------------------------------------------------------------------------
1296    // InvariantKind Tests
1297    // -------------------------------------------------------------------------
1298
1299    #[test]
1300    fn test_invariant_kind_serialization() {
1301        assert_eq!(
1302            serde_json::to_string(&InvariantKind::Type).unwrap(),
1303            "\"type\""
1304        );
1305        assert_eq!(
1306            serde_json::to_string(&InvariantKind::NonNull).unwrap(),
1307            "\"non_null\""
1308        );
1309        assert_eq!(
1310            serde_json::to_string(&InvariantKind::NonNegative).unwrap(),
1311            "\"non_negative\""
1312        );
1313    }
1314
1315    // -------------------------------------------------------------------------
1316    // Output Format Tests
1317    // -------------------------------------------------------------------------
1318
1319    #[test]
1320    fn test_output_format_default() {
1321        assert_eq!(OutputFormat::default(), OutputFormat::Json);
1322    }
1323
1324    #[test]
1325    fn test_output_format_display() {
1326        assert_eq!(OutputFormat::Json.to_string(), "json");
1327        assert_eq!(OutputFormat::Text.to_string(), "text");
1328    }
1329}