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
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
#![allow(unused)]
#![cfg_attr(coverage_nightly, coverage(off))]
//! Lightweight provability analysis using abstract interpretation
//!
//! This module provides fast, incremental provability analysis using abstract
//! interpretation techniques instead of heavyweight SMT solvers. It analyzes
//! code properties like null safety, bounds checking, aliasing, and purity
//! to compute a provability score that feeds into the TDG calculation.
//!
//! # Approach
//!
//! The analyzer uses abstract domains to track program properties:
//! - **Nullability Analysis**: Tracks potential null/undefined values
//! - **Interval Analysis**: Bounds checking and numeric ranges
//! - **Alias Analysis**: Detects potential aliasing issues
//! - **Purity Analysis**: Identifies side-effect free functions
//!
//! # Abstract Interpretation
//!
//! Instead of precise symbolic execution, we use:
//! - **Lattice-based Domains**: Fast join/meet operations
//! - **Widening**: Ensures termination for loops
//! - **Incremental Analysis**: Only re-analyze changed functions
//! - **Caching**: Persistent results across analysis runs
//!
//! # Integration with TDG
//!
//! The provability score (0.0-1.0) is converted to a factor (0.0-5.0) for TDG:
//! - Higher provability → Lower TDG score (more maintainable code)
//! - Lower provability → Higher TDG score (harder to reason about)
//!
//! # Example
//!
//! ```rust
//! use pmat::services::lightweight_provability_analyzer::{
//! LightweightProvabilityAnalyzer, FunctionId
//! };
//!
//! # async fn example() -> Result<(), Box<dyn std::error::Error>> {
//! let analyzer = LightweightProvabilityAnalyzer::new();
//!
//! // Analyze specific functions incrementally
//! let changed_functions = vec![
//! FunctionId {
//! file_path: "src/main.rs".to_string(),
//! function_name: "process_data".to_string(),
//! line_number: 42,
//! }
//! ];
//!
//! let summaries = analyzer.analyze_incrementally(&changed_functions).await;
//!
//! for summary in summaries {
//! println!("Provability score: {:.2}", summary.provability_score);
//! println!("Verified properties:");
//! for prop in &summary.verified_properties {
//! println!(" - {:?} (confidence: {:.0}%)",
//! prop.property_type, prop.confidence * 100.0);
//! }
//! }
//! # Ok(())
//! # }
//! ```
use std::sync::Arc;
use dashmap::DashMap;
use serde::{Deserialize, Serialize};
/// Lightweight Provability Analyzer using Abstract Interpretation
/// Replaces heavyweight SMT solver approach with dataflow analysis
pub struct LightweightProvabilityAnalyzer {
abstract_interpreter: AbstractInterpreter,
proof_cache: Arc<DashMap<FunctionId, ProofSummary>>,
current_version: u64,
}
#[derive(Clone, Debug, Hash, Eq, PartialEq)]
/// Function id.
pub struct FunctionId {
pub file_path: String,
pub function_name: String,
pub line_number: usize,
}
#[derive(Clone, Debug, Serialize, Deserialize)]
/// Summary of proof analysis.
pub struct ProofSummary {
pub provability_score: f64,
pub verified_properties: Vec<VerifiedProperty>,
pub analysis_time_us: u128,
pub version: u64,
}
#[derive(Clone, Debug, Serialize, Deserialize)]
/// Verified property.
pub struct VerifiedProperty {
pub property_type: PropertyType,
pub confidence: f64,
pub evidence: String,
}
#[derive(Clone, Debug, Serialize, Deserialize, PartialEq)]
/// Type classification for property.
pub enum PropertyType {
NullSafety,
BoundsCheck,
NoAliasing,
PureFunction,
MemorySafety,
ThreadSafety,
}
/// Abstract domain for property analysis
#[derive(Clone, Debug)]
pub struct PropertyDomain {
pub nullability: NullabilityLattice,
pub bounds: IntervalLattice,
pub aliasing: AliasLattice,
pub purity: PurityLattice,
}
#[derive(Clone, Debug, PartialEq)]
/// Nullability lattice.
pub enum NullabilityLattice {
Top, // Unknown
NotNull, // Definitely not null
MaybeNull, // Possibly null
Null, // Definitely null
Bottom, // Unreachable
}
#[derive(Clone, Debug)]
/// Interval lattice.
pub struct IntervalLattice {
pub lower: Option<i64>,
pub upper: Option<i64>,
}
#[derive(Clone, Debug, PartialEq)]
/// Alias lattice.
pub enum AliasLattice {
Top, // Unknown aliasing
NoAlias, // No aliasing
MayAlias, // May have aliases
MustAlias, // Definitely aliases
Bottom, // Unreachable
}
#[derive(Clone, Debug, PartialEq)]
/// Purity lattice.
pub enum PurityLattice {
Top, // Unknown purity
Pure, // Pure function
ReadOnly, // Only reads state
WriteLocal, // Only writes local state
WriteGlobal, // Writes global state
Bottom, // Unreachable
}
/// Abstract interpreter.
pub struct AbstractInterpreter {
analysis_depth: usize,
}
// Lattice join/meet/widen operations for PropertyDomain, NullabilityLattice,
// IntervalLattice, AliasLattice, and PurityLattice
include!("lightweight_provability_analyzer_lattice.rs");
// Core analysis: SourceFlags, LightweightProvabilityAnalyzer impl,
// AbstractInterpreter impl, Default impl
include!("lightweight_provability_analyzer_analysis.rs");
// Unit tests and property-based tests
include!("lightweight_provability_analyzer_tests.rs");