Port show_ide_info and skip_verification flags

Querying signatures, spans of call contract collection and call finding
does not work yet.
PR: viperproject#1334

prusti-interface/src/environment/diagnostic.rs

@@ -78,6 +78,15 @@ impl<'tcx> EnvDiagnostic<'tcx> {
         diagnostic.buffer(&mut self.warn_buffer.borrow_mut());
     }
 
+    /// Emits a note
+    pub fn span_note<S: Into<MultiSpan> + Clone>(
+        &self,
+        sp: S,
+        msg: &str
+    ) {
+        self.tcx.sess.span_note_without_error(sp, msg.to_string());
+    }
+
     /// Returns true if an error has been emitted
     pub fn has_errors(&self) -> bool {
         self.tcx.sess.has_errors().is_some()

prusti-interface/src/prusti_error.rs

@@ -20,7 +20,7 @@ use prusti_rustc_interface::{errors::MultiSpan, span::Span};
 /// `SpannedEncodingError` and similar types to something less confusing.)
 #[derive(Clone, Debug, PartialEq, Eq)]
 pub struct PrustiError {
-    kind: PrustiErrorKind,
+    kind: PrustiDiagnosticKind,
     /// If `true`, it should not be reported to the user. We need this in cases
     /// when the same error could be reported twice.
     ///
@@ -35,11 +35,12 @@ pub struct PrustiError {
 }
 /// Determines how a `PrustiError` is reported.
 #[derive(Clone, Debug, PartialEq, Eq)]
-pub enum PrustiErrorKind {
+pub enum PrustiDiagnosticKind {
     Error,
     Warning,
     /// A warning which is only shown if at least one error is emitted.
     WarningOnError,
+    Message,
 }
 
 impl PartialOrd for PrustiError {
@@ -60,7 +61,7 @@ impl PrustiError {
     /// Private constructor. Use one of the following methods.
     fn new(message: String, span: MultiSpan) -> Self {
         PrustiError {
-            kind: PrustiErrorKind::Error,
+            kind: PrustiDiagnosticKind::Error,
             is_disabled: false,
             message,
             span: Box::new(span),
@@ -114,7 +115,7 @@ impl PrustiError {
     pub fn warning<S: ToString>(message: S, span: MultiSpan) -> Self {
         check_message(message.to_string());
         let mut err = PrustiError::new(format!("[Prusti: warning] {}", message.to_string()), span);
-        err.kind = PrustiErrorKind::Warning;
+        err.kind = PrustiDiagnosticKind::Warning;
         err
     }
 
@@ -123,7 +124,7 @@ impl PrustiError {
     pub fn warning_on_error<S: ToString>(message: S, span: MultiSpan) -> Self {
         check_message(message.to_string());
         let mut err = PrustiError::new(format!("[Prusti: warning] {}", message.to_string()), span);
-        err.kind = PrustiErrorKind::WarningOnError;
+        err.kind = PrustiDiagnosticKind::WarningOnError;
         err
     }
 
@@ -146,13 +147,21 @@ impl PrustiError {
         error
     }
 
+    /// Report a message
+    pub fn message<S: ToString>(message: S, span: MultiSpan) -> Self {
+        check_message(message.to_string());
+        let mut msg = PrustiError::new(message.to_string(), span);
+        msg.kind = PrustiDiagnosticKind::Message;
+        msg
+    }
+
     /// Set that this Prusti error should be reported as a warning to the user
     pub fn set_warning(&mut self) {
-        self.kind = PrustiErrorKind::Warning;
+        self.kind = PrustiDiagnosticKind::Warning;
     }
 
     pub fn is_error(&self) -> bool {
-        matches!(self.kind, PrustiErrorKind::Error)
+        matches!(self.kind, PrustiDiagnosticKind::Error)
     }
 
     // FIXME: This flag is a temporary workaround for having duplicate errors
@@ -185,24 +194,28 @@ impl PrustiError {
     pub fn emit(self, env_diagnostic: &EnvDiagnostic) {
         assert!(!self.is_disabled);
         match self.kind {
-            PrustiErrorKind::Error => env_diagnostic.span_err_with_help_and_notes(
+            PrustiDiagnosticKind::Error => env_diagnostic.span_err_with_help_and_notes(
                 *self.span,
                 &self.message,
                 &self.help,
                 &self.notes,
             ),
-            PrustiErrorKind::Warning => env_diagnostic.span_warn_with_help_and_notes(
+            PrustiDiagnosticKind::Warning => env_diagnostic.span_warn_with_help_and_notes(
                 *self.span,
                 &self.message,
                 &self.help,
                 &self.notes,
             ),
-            PrustiErrorKind::WarningOnError => env_diagnostic.span_warn_on_err_with_help_and_notes(
+            PrustiDiagnosticKind::WarningOnError => env_diagnostic.span_warn_on_err_with_help_and_notes(
                 *self.span,
                 &self.message,
                 &self.help,
                 &self.notes,
             ),
+            PrustiDiagnosticKind::Message => env_diagnostic.span_note(
+                *self.span,
+                &self.message
+            ),
         };
     }
 

prusti-server/src/ide/encoding_info.rs

@@ -0,0 +1,14 @@
+use serde::Serialize;
+use super::vsc_span::VscSpan;
+
+#[derive(Serialize)]
+pub struct EncodingInfo {
+    pub call_contract_spans: String,
+}
+
+impl EncodingInfo {
+    pub fn to_json_string(self) -> String {
+        serde_json::to_string(&self).unwrap()
+    }
+}
+

prusti-server/src/ide/ide_verification_result.rs

@@ -0,0 +1,29 @@
+use serde::Serialize;
+use viper::VerificationResult;
+
+/// Generated for each verification item, containing information
+/// about the result of the verification. This information will be emitted
+/// if the show_ide_info flag is set, and it's purpose is to be
+/// consumed by prusti-assistant.
+#[derive(Serialize)]
+pub struct IdeVerificationResult {
+    /// the name / defpath of the method
+    item_name: String,
+    /// whether the verification of that method was successful
+    success: bool,
+    /// how long the verification took
+    time_ms: u128,
+    /// whether this result was cached or is fresh
+    cached: bool,
+}
+
+impl From<&VerificationResult> for IdeVerificationResult {
+    fn from(res: &VerificationResult) -> Self {
+        Self {
+            item_name: res.item_name.clone(),
+            success: res.is_success(),
+            time_ms: res.time_ms,
+            cached: res.cached,
+        }
+    }
+}

prusti-server/src/ide/mod.rs

@@ -0,0 +1,3 @@
+pub mod ide_verification_result;
+pub mod encoding_info;
+pub mod vsc_span;

prusti-server/src/ide/vsc_span.rs

@@ -0,0 +1,34 @@
+use prusti_rustc_interface::span::{source_map::SourceMap, Span};
+use serde::Serialize;
+
+/// a representation of spans that is more usable with VSCode.
+#[derive(Serialize, Clone)]
+pub struct VscSpan {
+    column_end: usize,
+    column_start: usize,
+    line_end: usize,
+    line_start: usize,
+    file_name: String,
+    is_primary: bool,
+}
+
+impl VscSpan {
+    pub fn from_span(sp: &Span, sourcemap: &SourceMap) -> Self {
+        let span_filename = sourcemap.span_to_filename(*sp);
+        let diag_filename = sourcemap.filename_for_diagnostics(&span_filename);
+        let file_name = format!("{diag_filename}");
+
+        let (l1, l2) = sourcemap.is_valid_span(*sp).expect("Invalid span");
+        Self {
+            column_start: l1.col.0,
+            column_end: l2.col.0,
+            line_start: l1.line,
+            line_end: l2.line,
+            file_name,
+            // the following one is not relevant here, we just want to be
+            // able to reuse the existing methods and the parser
+            // for spans in VSCode
+            is_primary: false,
+        }
+    }
+}

prusti-server/src/lib.rs

@@ -7,7 +7,6 @@
 #![warn(clippy::disallowed_types)]
 #![feature(rustc_private)]
 
-// use log::info;
 use ::log::{debug, error, info};
 use crate::{
     spawn_server_thread, PrustiClient, ServerMessage, VerificationRequest,
@@ -25,6 +24,7 @@ use prusti_rustc_interface::{
     errors::MultiSpan,
 };
 use viper::{self, PersistentCache, Viper};
+use ide::{encoding_info::EncodingInfo, ide_verification_result::IdeVerificationResult};
 use once_cell::sync::Lazy;
 
 mod client;
@@ -33,6 +33,7 @@ mod server;
 mod server_message;
 mod verification_request;
 mod backend;
+pub mod ide;
 
 pub use backend::*;
 pub use client::*;
@@ -68,6 +69,10 @@ pub fn verify_programs(
         (program_name, request)
     });
 
+    if config::show_ide_info() {
+        emit_contract_spans(env_diagnostic);
+    }
+
     let mut stopwatch = Stopwatch::start("prusti-server", "verifying Viper program");
     // runtime used either for client connecting to server sequentially
     // or to sequentially verify the requests -> single thread is sufficient
@@ -109,18 +114,39 @@ async fn handle_stream(
         }
     }
 
+    // if we are in an ide, we already emit the errors asynchronously, otherwise we wait for
+    // all of them because we want the errors to be reported sortedly
+    if !config::show_ide_info() {
+        prusti_errors.sort();
+
+        for prusti_error in prusti_errors {
+            debug!("Prusti error: {:?}", prusti_error);
+            prusti_error.emit(env_diagnostic);
+        }
+    }
+
     overall_result
 }
 
 fn handle_termination_message(
     env_diagnostic: &EnvDiagnostic<'_>,
-    // &self,
     program_name: String,
     result: viper::VerificationResult,
     prusti_errors: &mut Vec<PrustiError>,
     overall_result: &mut VerificationResult
 ) {
     debug!("Received termination message with result {result:?} in verification of {program_name}");
+    if config::show_ide_info() {
+        PrustiError::message(
+            format!(
+                "ideVerificationResult{}",
+                serde_json::to_string(&IdeVerificationResult::from(&result))
+                    .unwrap()
+            ),
+            DUMMY_SP.into(),
+        )
+        .emit(env_diagnostic);
+    }
     match result.kind {
         // nothing to do
         viper::VerificationResultKind::Success => (),
@@ -141,9 +167,9 @@ fn handle_termination_message(
                     program_name.clone(),
                     verification_error
                 );
-                // temporary error emition, delete when verification errors can be backtranslated again
+                // FIXME: temporary error emition, delete when the above is implemented again
                 env_diagnostic.span_err_with_help_and_notes(
-                    MultiSpan::new(),
+                    MultiSpan::from_span(DUMMY_SP.into()),
                     &format!(
                         "Verification error in {}: {:?}",
                         program_name.clone(),
@@ -197,3 +223,15 @@ fn verify_requests_local<'a>(
     };
     verification_stream.flatten()
 }
+
+pub fn emit_contract_spans(env_diagnostic: &EnvDiagnostic<'_>) {
+    let encoding_info = EncodingInfo {
+        // call_contract_spans: self.encoder.spans_of_call_contracts.borrow().to_vec(),
+        call_contract_spans: "call contract spans not implemented".to_string(),
+    };
+    PrustiError::message(
+        format!("encodingInfo{}", encoding_info.to_json_string()),
+        DUMMY_SP.into(),
+    )
+    .emit(env_diagnostic);
+}

prusti-utils/src/config.rs

@@ -170,6 +170,10 @@ lazy_static::lazy_static! {
         settings.set_default::<Vec<String>>("verify_only_basic_block_path", vec![]).unwrap();
         settings.set_default::<Vec<String>>("delete_basic_blocks", vec![]).unwrap();
 
+       // Flags specifically for Prusti-Assistant:
+        settings.set_default("show_ide_info", false).unwrap();
+        settings.set_default("skip_verification", false).unwrap();
+
         // Get the list of all allowed flags.
         let mut allowed_keys = get_keys(&settings);
         allowed_keys.insert("server_max_stored_verifiers".to_string());
@@ -1029,3 +1033,18 @@ pub fn enable_type_invariants() -> bool {
 pub fn test_free_pcs() -> bool {
     read_setting("test_free_pcs")
 }
+
+/// When enabled, prusti should return various Data structures that are
+/// used by prusti-assistant, such as a list of method calls,
+/// a list of all procedures to be verified, etc.
+pub fn show_ide_info() -> bool {
+    read_setting("show_ide_info")
+}
+
+/// When enabled, verification is skipped. Similar to no_verify but needed
+/// because no_verify is also set automatically for dependencies, independent
+/// of whether the user passed this flag. In general only required because
+/// of issue #1261
+pub fn skip_verification() -> bool {
+    read_setting("skip_verification")
+}

prusti/src/callbacks.rs

@@ -1,5 +1,5 @@
 use crate::{
-    ide_helper::fake_error::fake_error,
+    ide_helper::{compiler_info, fake_error::fake_error},
     verifier::verify,
 };
 use mir_state_analysis::test_free_pcs;
@@ -187,24 +187,24 @@ impl prusti_rustc_interface::driver::Callbacks for PrustiCompilerCalls {
             // that is already in `def_spec`?
             let (annotated_procedures, types) = env.get_annotated_procedures_and_types();
 
-            // if config::show_ide_info() && !config::no_verify() {
-            //     let compiler_info =
-            //         compiler_info::IdeInfo::collect(&env, &annotated_procedures, &def_spec);
-            //     let out = serde_json::to_string(&compiler_info).unwrap();
-            //     PrustiError::message(format!("compilerInfo{out}"), DUMMY_SP.into())
-            //         .emit(&env.diagnostic);
-            // }
+            if config::show_ide_info() && !config::no_verify() {
+                let compiler_info =
+                    compiler_info::IdeInfo::collect(&env, &annotated_procedures, &def_spec);
+                let out = serde_json::to_string(&compiler_info).unwrap();
+                PrustiError::message(format!("compilerInfo{out}"), DUMMY_SP.into())
+                    .emit(&env.diagnostic);
+            }
             // as long as we have to throw a fake error we need to check this
             let is_primary_package = std::env::var("CARGO_PRIMARY_PACKAGE").is_ok();
 
             // collect and output Information used by IDE:
-            if !config::no_verify() {
+            if !config::no_verify() && !config::skip_verification() {
                 let verification_task = VerificationTask {
                     procedures: annotated_procedures,
                     types,
                 };
                 verify(env, def_spec, verification_task);
-            } else if !config::no_verify() && is_primary_package {
+            } else if config::skip_verification() && !config::no_verify() && is_primary_package {
                 // add a fake error, reason explained in issue #1261
                 fake_error(&env);
             }