1  use crate::types::*;
  2  use anyhow::{anyhow, Result};
  3  use semver::Version;
  4  use std::collections::{HashMap, HashSet};
  5  use std::path::{Path, PathBuf};
  6  use std::sync::{Arc, RwLock};
  7  use tracing::{debug, error, info, warn};
  8  use uuid::Uuid;
  9  
 10  /// Stable ABI trait for verification plugins
 11  ///
 12  /// This trait defines the interface that all verification plugins must implement.
 13  /// The ABI is designed to be stable across minor version updates to ensure
 14  /// plugin compatibility.
 15  pub trait VerificationPlugin: Send + Sync {
 16      /// Plugin name and identifier
 17      fn name(&self) -> &str;
 18  
 19      /// Plugin version (semantic versioning)
 20      fn version(&self) -> &str;
 21  
 22      /// List of verification techniques supported by this plugin
 23      fn supported_techniques(&self) -> Vec<Technique>;
 24  
 25      /// Minimum and maximum supported FerrisProof versions
 26      fn supported_versions(&self) -> VersionRange;
 27  
 28      /// Check if the tool is available and properly configured
 29      fn check_availability(&self) -> Result<ToolInfo>;
 30  
 31      /// Execute verification with given input
 32      fn verify(&self, input: VerificationInput) -> Result<VerificationOutput>;
 33  
 34      /// Parse tool output into structured results
 35      fn parse_output(&self, raw_output: &str) -> Result<StructuredResult>;
 36  
 37      /// Get plugin metadata and capabilities
 38      fn metadata(&self) -> PluginMetadata;
 39  
 40      /// Initialize plugin with configuration
 41      fn initialize(&mut self, config: &serde_json::Value) -> Result<()>;
 42  
 43      /// Cleanup plugin resources
 44      fn cleanup(&mut self) -> Result<()>;
 45  }
 46  
 47  #[derive(Debug, Clone)]
 48  pub struct ToolValidationResult {
 49      pub plugin_name: String,
 50      pub tool_info: Option<ToolInfo>,
 51      pub status: ValidationStatus,
 52      pub issues: Vec<String>,
 53  }
 54  
 55  #[derive(Debug, Clone, PartialEq, Eq)]
 56  pub enum ValidationStatus {
 57      Valid,
 58      Unavailable,
 59      VersionIncompatible,
 60      Error,
 61  }
 62  
 63  #[derive(Debug, Clone)]
 64  pub struct ToolInfo {
 65      pub name: String,
 66      pub version: String,
 67      pub path: PathBuf,
 68      pub available: bool,
 69      pub capabilities: Vec<String>,
 70  }
 71  
 72  #[derive(Debug, Clone)]
 73  pub struct VerificationInput {
 74      pub target: crate::verification::Target,
 75      pub config: EffectiveConfig,
 76      pub context: VerificationContext,
 77  }
 78  
 79  #[derive(Debug, Clone)]
 80  pub struct VerificationOutput {
 81      pub status: Status,
 82      pub violations: Vec<Violation>,
 83      pub artifacts: Vec<Artifact>,
 84      pub tool_output: ToolOutput,
 85      pub metrics: VerificationMetrics,
 86  }
 87  
 88  #[derive(Debug, Clone)]
 89  pub struct EffectiveConfig {
 90      pub level: VerificationLevel,
 91      pub enforcement: EnforcementMode,
 92      pub enabled_techniques: Vec<Technique>,
 93      pub tool_config: serde_json::Value,
 94  }
 95  
 96  #[derive(Debug, Clone)]
 97  pub struct VerificationContext {
 98      pub session_id: String,
 99      pub working_dir: PathBuf,
100      pub cache_dir: PathBuf,
101      pub timeout: Option<std::time::Duration>,
102      pub parallel_id: Option<u32>,
103  }
104  
105  #[derive(Debug, Clone)]
106  pub struct PluginMetadata {
107      pub name: String,
108      pub version: String,
109      pub description: String,
110      pub author: String,
111      pub license: String,
112      pub homepage: Option<String>,
113      pub techniques: Vec<Technique>,
114      pub supported_platforms: Vec<String>,
115      pub dependencies: Vec<String>,
116  }
117  
118  #[derive(Debug, Clone)]
119  pub struct VersionRange {
120      pub min: Option<Version>,
121      pub max: Option<Version>,
122      pub requires_exact: Option<Version>,
123  }
124  
125  #[derive(Debug, Clone)]
126  pub struct StructuredResult {
127      pub status: Status,
128      pub violations: Vec<Violation>,
129      pub statistics: serde_json::Value,
130      pub performance: PerformanceMetrics,
131  }
132  
133  #[derive(Debug, Clone)]
134  pub struct PerformanceMetrics {
135      pub execution_time: std::time::Duration,
136      pub memory_usage: u64,
137      pub cpu_usage: f64,
138      pub cache_hits: u32,
139  }
140  
141  pub struct PluginManager {
142      plugins: HashMap<String, Arc<RwLock<Box<dyn VerificationPlugin>>>>,
143      plugin_registry: PluginRegistry,
144      version_checker: VersionChecker,
145      discovery: PluginDiscovery,
146  }
147  
148  #[derive(Debug, Default)]
149  struct PluginRegistry {
150      registered_plugins: HashMap<String, PluginRegistration>,
151      loaded_plugins: HashSet<String>,
152  }
153  
154  #[derive(Debug, Clone)]
155  #[allow(dead_code)]
156  struct PluginRegistration {
157      metadata: PluginMetadata,
158      library_path: PathBuf,
159      version_compatible: bool,
160  }
161  
162  #[derive(Debug)]
163  struct VersionChecker {
164      current_version: Version,
165  }
166  
167  #[derive(Debug)]
168  struct PluginDiscovery {
169      search_paths: Vec<PathBuf>,
170  }
171  
172  impl PluginManager {
173      pub fn new() -> Self {
174          let current_version = Version::parse(env!("CARGO_PKG_VERSION"))
175              .expect("Failed to parse current FerrisProof version");
176  
177          Self {
178              plugins: HashMap::new(),
179              plugin_registry: PluginRegistry::default(),
180              version_checker: VersionChecker::new(current_version),
181              discovery: PluginDiscovery::new(),
182          }
183      }
184  
185      /// Register a plugin instance
186      pub fn register_plugin(&mut self, plugin: Box<dyn VerificationPlugin>) -> Result<()> {
187          let name = plugin.name().to_string();
188          let version = plugin.version().to_string();
189  
190          // Check version compatibility
191          let version_range = plugin.supported_versions();
192          if !self.version_checker.is_compatible(&version_range) {
193              return Err(anyhow!(
194                  "Plugin {} version {} is not compatible with FerrisProof {}",
195                  name,
196                  version,
197                  self.version_checker.current_version
198              ));
199          }
200  
201          let plugin_arc = Arc::new(RwLock::new(plugin));
202          self.plugins.insert(name.clone(), plugin_arc);
203  
204          info!("Registered plugin: {} v{}", name, version);
205          Ok(())
206      }
207  
208      /// Discover and load plugins from search paths
209      pub fn discover_plugins(&mut self) -> Result<usize> {
210          info!("Discovering plugins in search paths");
211  
212          let mut discovered_count = 0;
213  
214          // Collect search paths to avoid borrowing issues
215          let search_paths: Vec<PathBuf> = self.discovery.search_paths.clone();
216  
217          for search_path in &search_paths {
218              if search_path.exists() {
219                  discovered_count += self.discover_in_directory(search_path)?;
220              }
221          }
222  
223          info!("Discovered {} plugins", discovered_count);
224          Ok(discovered_count)
225      }
226  
227      /// Discover plugins in a specific directory
228      fn discover_in_directory(&mut self, dir: &Path) -> Result<usize> {
229          let mut discovered_count = 0;
230  
231          for entry in std::fs::read_dir(dir)? {
232              let entry = entry?;
233              let path = entry.path();
234  
235              // Look for plugin manifest files
236              if path.extension().and_then(|s| s.to_str()) == Some("json") {
237                  match self.load_plugin_from_manifest(&path) {
238                      Ok(_) => discovered_count += 1,
239                      Err(e) => {
240                          warn!("Failed to load plugin from manifest {:?}: {}", path, e);
241                      }
242                  }
243              }
244          }
245  
246          Ok(discovered_count)
247      }
248  
249      /// Load plugin from manifest file
250      fn load_plugin_from_manifest(&mut self, manifest_path: &Path) -> Result<()> {
251          let manifest_content = std::fs::read_to_string(manifest_path)?;
252          let manifest: serde_json::Value = serde_json::from_str(&manifest_content)?;
253  
254          let metadata = PluginMetadata::from_json(&manifest)?;
255  
256          // Check if already loaded
257          if self.plugin_registry.loaded_plugins.contains(&metadata.name) {
258              return Ok(());
259          }
260  
261          // For now, just register the metadata
262          // TODO: Implement dynamic loading with libloading
263          let registration = PluginRegistration {
264              metadata: metadata.clone(),
265              library_path: manifest_path
266                  .parent()
267                  .unwrap_or_else(|| Path::new("."))
268                  .join(format!("lib{}.so", metadata.name)),
269              version_compatible: self.version_checker.is_metadata_compatible(&metadata),
270          };
271  
272          self.plugin_registry
273              .registered_plugins
274              .insert(metadata.name.clone(), registration);
275  
276          info!("Discovered plugin: {} v{}", metadata.name, metadata.version);
277          Ok(())
278      }
279  
280      /// Get all plugins that support a specific technique
281      pub fn plugins_for_technique(
282          &self,
283          technique: &Technique,
284      ) -> Vec<Arc<RwLock<Box<dyn VerificationPlugin>>>> {
285          self.plugins
286              .values()
287              .filter(|plugin| {
288                  let plugin_guard = plugin.read().ok();
289                  if let Some(plugin) = plugin_guard {
290                      plugin.supported_techniques().contains(technique)
291                  } else {
292                      false
293                  }
294              })
295              .cloned()
296              .collect()
297      }
298  
299      /// Validate all registered tools and their versions
300      pub fn validate_tools(&self) -> Result<Vec<ToolValidationResult>> {
301          let mut validation_results = Vec::new();
302  
303          for (name, plugin) in &self.plugins {
304              match plugin.read() {
305                  Ok(plugin) => {
306                      let validation_result = match plugin.check_availability() {
307                          Ok(tool_info) => {
308                              // Validate tool version if plugin specifies requirements
309                              let version_validation =
310                                  self.version_checker.validate_tool_version(&tool_info, None);
311  
312                              match version_validation {
313                                  Ok(_) => {
314                                      debug!("Tool {} is available and compatible", name);
315                                      ToolValidationResult {
316                                          plugin_name: name.clone(),
317                                          tool_info: Some(tool_info),
318                                          status: ValidationStatus::Valid,
319                                          issues: Vec::new(),
320                                      }
321                                  }
322                                  Err(e) => {
323                                      warn!("Tool {} version incompatible: {}", name, e);
324                                      ToolValidationResult {
325                                          plugin_name: name.clone(),
326                                          tool_info: Some(tool_info),
327                                          status: ValidationStatus::VersionIncompatible,
328                                          issues: vec![e.to_string()],
329                                      }
330                                  }
331                              }
332                          }
333                          Err(e) => {
334                              warn!("Tool {} not available: {}", name, e);
335                              ToolValidationResult {
336                                  plugin_name: name.clone(),
337                                  tool_info: None,
338                                  status: ValidationStatus::Unavailable,
339                                  issues: vec![e.to_string()],
340                              }
341                          }
342                      };
343  
344                      validation_results.push(validation_result);
345                  }
346                  Err(e) => {
347                      error!("Failed to lock plugin {}: {}", name, e);
348                      validation_results.push(ToolValidationResult {
349                          plugin_name: name.clone(),
350                          tool_info: None,
351                          status: ValidationStatus::Error,
352                          issues: vec![format!("Plugin lock error: {}", e)],
353                      });
354                  }
355              }
356          }
357  
358          Ok(validation_results)
359      }
360  
361      /// Execute verification using appropriate plugin
362      pub async fn verify(
363          &self,
364          technique: &Technique,
365          input: VerificationInput,
366      ) -> Result<VerificationOutput> {
367          let plugins = self.plugins_for_technique(technique);
368  
369          if plugins.is_empty() {
370              return Err(anyhow!(
371                  "No plugins available for technique: {:?}",
372                  technique
373              ));
374          }
375  
376          // Use first available plugin
377          // TODO: Implement plugin selection strategy
378          if let Some(plugin_arc) = plugins.first() {
379              let plugin = plugin_arc
380                  .read()
381                  .map_err(|e| anyhow!("Failed to acquire plugin lock: {}", e))?;
382  
383              // Create verification context
384              let context = VerificationContext {
385                  session_id: Uuid::new_v4().to_string(),
386                  working_dir: std::env::current_dir().unwrap_or_else(|_| PathBuf::from("/tmp")),
387                  cache_dir: std::env::temp_dir(),
388                  timeout: Some(std::time::Duration::from_secs(300)), // 5 minutes default
389                  parallel_id: None,
390              };
391  
392              let enhanced_input = VerificationInput {
393                  target: input.target,
394                  config: input.config,
395                  context,
396              };
397  
398              plugin.verify(enhanced_input)
399          } else {
400              Err(anyhow!(
401                  "No plugin available for technique: {:?}",
402                  technique
403              ))
404          }
405      }
406  
407      /// Get plugin metadata
408      pub fn plugin_metadata(&self, name: &str) -> Option<PluginMetadata> {
409          if let Some(plugin_arc) = self.plugins.get(name) {
410              match plugin_arc.read() {
411                  Ok(plugin) => Some(plugin.metadata()),
412                  Err(_) => None,
413              }
414          } else {
415              self.plugin_registry
416                  .registered_plugins
417                  .get(name)
418                  .map(|registration| registration.metadata.clone())
419          }
420      }
421  
422      /// List all registered plugins
423      pub fn list_plugins(&self) -> Vec<PluginMetadata> {
424          let mut metadata_list = Vec::new();
425  
426          // Add loaded plugins
427          for (name, plugin_arc) in &self.plugins {
428              match plugin_arc.read() {
429                  Ok(plugin) => {
430                      metadata_list.push(plugin.metadata());
431                  }
432                  Err(_) => {
433                      warn!("Failed to read plugin metadata for: {}", name);
434                  }
435              }
436          }
437  
438          // Add discovered but not loaded plugins
439          for registration in self.plugin_registry.registered_plugins.values() {
440              if !self
441                  .plugin_registry
442                  .loaded_plugins
443                  .contains(&registration.metadata.name)
444              {
445                  metadata_list.push(registration.metadata.clone());
446              }
447          }
448  
449          metadata_list.sort_by(|a, b| a.name.cmp(&b.name));
450          metadata_list
451      }
452  
453      /// Initialize all plugins with configuration
454      pub fn initialize_plugins(&mut self, config: &serde_json::Value) -> Result<()> {
455          for (name, plugin_arc) in &self.plugins {
456              match plugin_arc.write() {
457                  Ok(mut plugin) => {
458                      if let Some(plugin_config) = config.get(name) {
459                          if let Err(e) = plugin.initialize(plugin_config) {
460                              warn!("Failed to initialize plugin {}: {}", name, e);
461                          }
462                      }
463                  }
464                  Err(e) => {
465                      error!("Failed to acquire write lock for plugin {}: {}", name, e);
466                  }
467              }
468          }
469          Ok(())
470      }
471  
472      /// Cleanup all plugins
473      pub fn cleanup_plugins(&mut self) -> Result<()> {
474          for (name, plugin_arc) in &self.plugins {
475              match plugin_arc.write() {
476                  Ok(mut plugin) => {
477                      if let Err(e) = plugin.cleanup() {
478                          warn!("Failed to cleanup plugin {}: {}", name, e);
479                      }
480                  }
481                  Err(e) => {
482                      error!("Failed to acquire write lock for plugin {}: {}", name, e);
483                  }
484              }
485          }
486          Ok(())
487      }
488  }
489  
490  impl PluginMetadata {
491      fn from_json(value: &serde_json::Value) -> Result<Self> {
492          Ok(Self {
493              name: value
494                  .get("name")
495                  .and_then(|v| v.as_str())
496                  .ok_or_else(|| anyhow!("Missing plugin name"))?
497                  .to_string(),
498              version: value
499                  .get("version")
500                  .and_then(|v| v.as_str())
501                  .ok_or_else(|| anyhow!("Missing plugin version"))?
502                  .to_string(),
503              description: value
504                  .get("description")
505                  .and_then(|v| v.as_str())
506                  .unwrap_or("No description available")
507                  .to_string(),
508              author: value
509                  .get("author")
510                  .and_then(|v| v.as_str())
511                  .unwrap_or("Unknown")
512                  .to_string(),
513              license: value
514                  .get("license")
515                  .and_then(|v| v.as_str())
516                  .unwrap_or("Unknown")
517                  .to_string(),
518              homepage: value
519                  .get("homepage")
520                  .and_then(|v| v.as_str())
521                  .map(|s| s.to_string()),
522              techniques: value
523                  .get("techniques")
524                  .and_then(|v| v.as_array())
525                  .map(|arr| {
526                      arr.iter()
527                          .filter_map(|v| v.as_str())
528                          .filter_map(|s| match s {
529                              "TypeSafety" => Some(Technique::TypeSafety),
530                              "PropertyTests" => Some(Technique::PropertyTests),
531                              "SessionTypes" => Some(Technique::SessionTypes),
532                              "RefinementTypes" => Some(Technique::RefinementTypes),
533                              "ConcurrencyTesting" => Some(Technique::ConcurrencyTesting),
534                              "FormalSpecs" => Some(Technique::FormalSpecs),
535                              "ModelChecking" => Some(Technique::ModelChecking),
536                              _ => None,
537                          })
538                          .collect()
539                  })
540                  .unwrap_or_default(),
541              supported_platforms: value
542                  .get("platforms")
543                  .and_then(|v| v.as_array())
544                  .map(|arr| {
545                      arr.iter()
546                          .filter_map(|v| v.as_str())
547                          .map(|s| s.to_string())
548                          .collect()
549                  })
550                  .unwrap_or_default(),
551              dependencies: value
552                  .get("dependencies")
553                  .and_then(|v| v.as_array())
554                  .map(|arr| {
555                      arr.iter()
556                          .filter_map(|v| v.as_str())
557                          .map(|s| s.to_string())
558                          .collect()
559                  })
560                  .unwrap_or_default(),
561          })
562      }
563  }
564  
565  impl PluginRegistry {
566      #[allow(dead_code)]
567      fn register(&mut self, name: String, registration: PluginRegistration) {
568          self.registered_plugins.insert(name, registration);
569      }
570  }
571  
572  impl VersionChecker {
573      fn new(current_version: Version) -> Self {
574          Self { current_version }
575      }
576  
577      /// Check if a plugin's version range is compatible with current FerrisProof version
578      fn is_compatible(&self, version_range: &VersionRange) -> bool {
579          if let Some(exact_version) = &version_range.requires_exact {
580              return &self.current_version == exact_version;
581          }
582  
583          if let Some(min_version) = &version_range.min {
584              if self.current_version < *min_version {
585                  return false;
586              }
587          }
588  
589          if let Some(max_version) = &version_range.max {
590              if self.current_version > *max_version {
591                  return false;
592              }
593          }
594  
595          true
596      }
597  
598      /// Check if plugin metadata indicates compatibility
599      fn is_metadata_compatible(&self, metadata: &PluginMetadata) -> bool {
600          // Check plugin metadata version compatibility
601          if let Ok(plugin_version) = metadata.version.parse::<Version>() {
602              // Check if plugin version is within reasonable bounds
603              // Allow plugins that are at most 1 major version behind or ahead
604              let major_diff = (self.current_version.major as i64) - (plugin_version.major as i64);
605              major_diff.abs() <= 1
606          } else {
607              false
608          }
609      }
610  
611      /// Validate tool version compatibility
612      fn validate_tool_version(
613          &self,
614          tool_info: &ToolInfo,
615          expected_range: Option<&VersionRange>,
616      ) -> Result<()> {
617          if let Some(range) = expected_range {
618              if let Ok(tool_version) = tool_info.version.parse::<Version>() {
619                  if let Some(min_version) = &range.min {
620                      if tool_version < *min_version {
621                          return Err(anyhow!(
622                              "Tool {} version {} is below minimum required version {}",
623                              tool_info.name,
624                              tool_version,
625                              min_version
626                          ));
627                      }
628                  }
629  
630                  if let Some(max_version) = &range.max {
631                      if tool_version > *max_version {
632                          return Err(anyhow!(
633                              "Tool {} version {} is above maximum supported version {}",
634                              tool_info.name,
635                              tool_version,
636                              max_version
637                          ));
638                      }
639                  }
640  
641                  if let Some(exact_version) = &range.requires_exact {
642                      if tool_version != *exact_version {
643                          return Err(anyhow!(
644                              "Tool {} version {} does not match required exact version {}",
645                              tool_info.name,
646                              tool_version,
647                              exact_version
648                          ));
649                      }
650                  }
651              } else {
652                  warn!("Could not parse tool version: {}", tool_info.version);
653              }
654          }
655  
656          Ok(())
657      }
658  }
659  
660  impl PluginDiscovery {
661      fn new() -> Self {
662          let mut search_paths = Vec::new();
663  
664          // Add default search paths
665          if let Some(home_dir) = dirs::home_dir() {
666              search_paths.push(home_dir.join(".ferris-proof/plugins"));
667              search_paths.push(home_dir.join(".local/share/ferris-proof/plugins"));
668          }
669  
670          if let Ok(current_dir) = std::env::current_dir() {
671              search_paths.push(current_dir.join(".ferris-proof/plugins"));
672          }
673  
674          // Add system-wide paths
675          search_paths.push(PathBuf::from("/usr/local/lib/ferris-proof/plugins"));
676          search_paths.push(PathBuf::from("/usr/lib/ferris-proof/plugins"));
677  
678          Self { search_paths }
679      }
680  }
681  
682  impl Default for PluginManager {
683      fn default() -> Self {
684          Self::new()
685      }
686  }