[WIP] Various IDE improvements and new features

docs/dev-guide/src/config/flags.md

@@ -55,18 +55,25 @@
 | [`PRINT_DESUGARED_SPECS`](#print_desugared_specs) | `bool` | `false` | A |
 | [`PRINT_HASH`](#print_hash) | `bool` | `false` | A |
 | [`PRINT_TYPECKD_SPECS`](#print_typeckd_specs) | `bool` | `false` | A |
+| [`QUERY_METHOD_SIGNATURE`](#query_method_signature) | `Option<String>` | `None` | A |
 | [`QUIET`](#quiet) | `bool` | `false` | A* |
+| [`REPORT_VIPER_MESSAGES`](#report_viper_messages) | `bool` | `false` | A |
+| [`VERIFY_ONLY_DEFPATH`](#verify_only_defpath) | `Option<String>` | `None` | A |
 | [`SERVER_ADDRESS`](#server_address) | `Option<String>` | `None` | A |
 | [`SERVER_MAX_CONCURRENCY`](#server_max_concurrency) | `Option<usize>` | `None` | A |
 | [`SERVER_MAX_STORED_VERIFIERS`](#server_max_stored_verifiers) | `Option<usize>` | `None` | A |
+| [`SHOW_IDE_INFO`](#show_ide_info) | `bool` | `false` | A |
 | [`SIMPLIFY_ENCODING`](#simplify_encoding) | `bool` | `true` | A |
 | [`SKIP_UNSUPPORTED_FEATURES`](#skip_unsupported_features) | `bool` | `false` | A |
+| [`SKIP_VERIFICATION`](#skip_verification) | `bool` | `false` | A |
 | [`SMT_QI_BOUND_GLOBAL`](#smt_qi_bound_global) | `Option<u64>` | `None` | A |
-[`SMT_QI_BOUND_GLOBAL_KIND`](#smt_qi_bound_global_kind) | `Option<u64>` | `None` | A |
+| [`SMT_QI_BOUND_GLOBAL_KIND`](#smt_qi_bound_global_kind) | `Option<u64>` | `None` | A |
 | [`SMT_QI_BOUND_TRACE`](#smt_qi_bound_trace) | `Option<u64>` | `None` | A |
 | [`SMT_QI_BOUND_TRACE_KIND`](#smt_qi_bound_trace_kind) | `Option<u64>` | `None` | A |
-| [`SMT_QI_IGNORE_BUILTIN`](#smt_qi_ignore_builtin) | `bool` | `true` | A |
 | [`SMT_QI_EAGER_THRESHOLD`](#smt_qi_eager_threshold) | `u64` | `1000` | A |
+| [`SMT_QI_IGNORE_BUILTIN`](#smt_qi_ignore_builtin) | `bool` | `true` | A |
+| [`SMT_QI_PROFILE`](#smt_qi_profile) | `Option<bool>` | `None` | A |
+| [`SMT_QI_PROFILE_FREQ`](#smt_qi_profile_freq) | `Option<u64>` | `None` | A |
 | [`SMT_SOLVER_PATH`](#smt_solver_path) | `Option<String>` | `env::var("Z3_EXE")` | A |
 | [`SMT_SOLVER_WRAPPER_PATH`](#smt_solver_wrapper_path) | `Option<String>` | `None` | A |
 | [`SMT_UNIQUE_TRIGGERS_BOUND`](#smt_unique_triggers_bound) | `Option<u64>` | `None` | A |
@@ -351,12 +358,24 @@ When enabled, prints the hash of a verification request (the hash is used for ca
 
 When enabled, prints the type-checked specifications.
 
+## `QUERY_METHOD_SIGNATURE`
+
+When set to a defpath, prusti will generate a template for an external specification for this method. The result is part of the CompilerInfo and will only be emitted if the `SHOW_IDE_INFO` flag is enabled too.
+
 ## `QUIET`
 
 When enabled, user messages are not printed. Otherwise, messages output into `stderr`.
 
 > **Note:** `cargo prusti` sets this flag with `DEFAULT_PRUSTI_QUIET=true`.
 
+## `REPORT_VIPER_MESSAGES`
+
+When enabled for both server and client, certain supported Viper messages will be reported to the user.
+
+## `VERIFY_ONLY_DEFPATH`
+
+When set to the defpath of a local method, prusti will only verify the specified method. A fake error will be generated to avoid caching of a success.
+
 ## `SERVER_ADDRESS`
 
 When set to an address and port (e.g. `"127.0.0.1:2468"`), Prusti will connect to the given server and use it for its verification backend.
@@ -373,6 +392,10 @@ Maximum amount of instantiated Viper verifiers the server will keep around for r
 
 > **Note:** This does _not_ limit how many verification requests the server handles concurrently, only the size of what is essentially its verifier cache.
 
+## `SHOW_IDE_INFO`
+
+When enabled, we emit various json data structures containing information about the program, its encoding, and the results of the verification. This flag intended for prusti-assistant (IDE).
+
 ## `SIMPLIFY_ENCODING`
 
 When enabled, the encoded program is simplified before it is passed to the Viper backend.
@@ -381,6 +404,10 @@ When enabled, the encoded program is simplified before it is passed to the Viper
 
 When enabled, features not supported by Prusti will be reported as warnings rather than errors.
 
+## `SKIP_VERIFICATION`
+
+When enabled, verification will be skipped. Opposed to `NO_VERIFY`, this flag will cause fake errors to stop the compiler from caching the result. 
+
 ## `SMT_QI_BOUND_GLOBAL`
 
 If not `None`, checks that the number of global quantifier instantiations reported by the SMT wrapper is smaller than the specified bound.
@@ -408,6 +435,13 @@ If not `None`, checks that the number of quantifier instantiations in each trace
 ## `SMT_QI_IGNORE_BUILTIN`
 
 When enabled, ignores the built-in quantifiers in SMT quantifier instantiation bounds checking.
+## `SMT_QI_PROFILE`
+
+When enabled, the Z3 backend periodically (and on finish) reports the number of quantifier instantiations to Viper.
+
+## `SMT_QI_PROFILE_FREQ`
+
+Frequency of the quantifier instantiation reporting of Z3 (every X instantiations, a report is issued).
 
 ## `SMT_QI_EAGER_THRESHOLD`
 

prusti-common/src/vir/program_normalization.rs

@@ -7,8 +7,9 @@
 use crate::vir::{program::Program, Position};
 use log::{debug, trace};
 use rustc_hash::{FxHashMap, FxHashSet};
-use viper::VerificationResult;
+use viper::VerificationResultKind;
 
+#[derive(Clone)]
 pub enum NormalizationInfo {
     LegacyProgram { original_position_ids: Vec<u64> },
     LowProgram,
@@ -103,8 +104,8 @@ impl NormalizationInfo {
     }
 
     /// Denormalize a verification result.
-    pub fn denormalize_result(&self, result: &mut VerificationResult) {
-        if let VerificationResult::Failure(ref mut ver_errors) = result {
+    pub fn denormalize_result(&self, result: &mut VerificationResultKind) {
+        if let VerificationResultKind::Failure(ref mut ver_errors) = result {
             ver_errors.iter_mut().for_each(|ver_error| {
                 if let Some(pos) = ver_error.pos_id.as_mut() {
                     self.denormalize_position_string(pos);

prusti-interface/src/environment/diagnostic.rs

@@ -78,6 +78,11 @@ 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);
+    }
+
     /// 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,26 @@ 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(
-                *self.span,
-                &self.message,
-                &self.help,
-                &self.notes,
-            ),
-            PrustiErrorKind::Warning => env_diagnostic.span_warn_with_help_and_notes(
+            PrustiDiagnosticKind::Error => env_diagnostic.span_err_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::Warning => env_diagnostic.span_warn_with_help_and_notes(
                 *self.span,
                 &self.message,
                 &self.help,
                 &self.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/Cargo.toml

@@ -19,6 +19,7 @@ doctest = false
 [dependencies]
 log = { version = "0.4", features = ["release_max_level_info"] }
 viper = { path = "../viper" }
+viper-sys = { path = "../viper-sys" }
 prusti-common = { path = "../prusti-common" }
 prusti-utils = { path = "../prusti-utils" }
 tracing = { path = "../tracing" }
@@ -28,11 +29,18 @@ bincode = "1.0"
 url = "2.2.2"
 num_cpus = "1.14"
 serde = { version = "1.0", features = ["derive"] }
+serde_json = { version = "1.0" }
+tokio = "1.20"
+jni = { version = "0.20", features = ["invocation"] }
+# the tungstenite version used by warp 0.3
+tokio-tungstenite = "0.13"
+futures = "0.3.25"
+futures-util = "0.3.25"
+async-stream = "0.3.3"
+once_cell = "1.17.0"
 reqwest = { version = "0.11", default-features = false, features = ["json", "rustls-tls"] }
 warp = "0.3"
-tokio = "1.20"
 rustc-hash = "1.1.0"
-once_cell = "1.17.1"
 
 [dev-dependencies]
 lazy_static = "1.4.0"