From 5270e09a80ec6dd5e8ec9d456b342cffe74600fb Mon Sep 17 00:00:00 2001 From: trk Date: Thu, 13 Jun 2024 15:13:15 +0200 Subject: [PATCH] Port `verify_only_defpath` and `report_viper_messages` flags Defpath only verification does not work since test_entrypoint currently just puts the entire program into the request regardless of the verification tasks at hand. Update the flags in the documentation. PR: https://github.com/viperproject/prusti-dev/pull/1334 --- docs/dev-guide/src/config/flags.md | 26 +++++++++++- prusti-server/src/backend.rs | 64 +++++++++++++++++++++++++++++- prusti-server/src/lib.rs | 1 - prusti-utils/src/config.rs | 14 +++++++ prusti/src/callbacks.rs | 32 ++++++++++++--- 5 files changed, 129 insertions(+), 8 deletions(-) diff --git a/docs/dev-guide/src/config/flags.md b/docs/dev-guide/src/config/flags.md index b3ef1913dc9..7472db5ca94 100644 --- a/docs/dev-guide/src/config/flags.md +++ b/docs/dev-guide/src/config/flags.md @@ -56,13 +56,16 @@ | [`PRINT_HASH`](#print_hash) | `bool` | `false` | A | | [`PRINT_TYPECKD_SPECS`](#print_typeckd_specs) | `bool` | `false` | A | | [`QUIET`](#quiet) | `bool` | `false` | A* | +| [`REPORT_VIPER_MESSAGES`](#report_viper_messages) | `bool` | `false` | A | | [`SERVER_ADDRESS`](#server_address) | `Option` | `None` | A | | [`SERVER_MAX_CONCURRENCY`](#server_max_concurrency) | `Option` | `None` | A | | [`SERVER_MAX_STORED_VERIFIERS`](#server_max_stored_verifiers) | `Option` | `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` | `None` | A | -[`SMT_QI_BOUND_GLOBAL_KIND`](#smt_qi_bound_global_kind) | `Option` | `None` | A | +| [`SMT_QI_BOUND_GLOBAL_KIND`](#smt_qi_bound_global_kind) | `Option` | `None` | A | | [`SMT_QI_BOUND_TRACE`](#smt_qi_bound_trace) | `Option` | `None` | A | | [`SMT_QI_BOUND_TRACE_KIND`](#smt_qi_bound_trace_kind) | `Option` | `None` | A | | [`SMT_QI_IGNORE_BUILTIN`](#smt_qi_ignore_builtin) | `bool` | `true` | A | @@ -76,6 +79,7 @@ | [`USE_SMT_WRAPPER`](#use_smt_wrapper) | `bool` | `false` | A | | [`VERIFICATION_DEADLINE`](#verification_deadline) | `Option` | `None` | A | | [`VERIFY_ONLY_BASIC_BLOCK_PATH`](#verify_only_basic_block_path) | `Vec` | `vec![]` | A | +| [`VERIFY_ONLY_DEFPATH`](#verify_only_defpath) | `Option` | `None` | A | | [`VERIFY_ONLY_PREAMBLE`](#verify_only_preamble) | `bool` | `false` | A | | [`VIPER_BACKEND`](#viper_backend) | `String` | `"Silicon"` | A | | [`VIPER_HOME`](#viper_home) | `Option` | `None` | A | @@ -357,6 +361,14 @@ When enabled, user messages are not printed. Otherwise, messages output into `st > **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 +385,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 +397,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. @@ -468,6 +488,10 @@ Verify only the single execution path goes through the given basic blocks. All b > **Note:** This option is only for debugging Prusti. +## `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. + ## `VERIFY_ONLY_PREAMBLE` When enabled, only the preamble will be verified: domains, functions, and predicates. diff --git a/prusti-server/src/backend.rs b/prusti-server/src/backend.rs index d0445f233a5..c5e0f942e32 100644 --- a/prusti-server/src/backend.rs +++ b/prusti-server/src/backend.rs @@ -51,9 +51,71 @@ impl<'a> Backend<'a> { stopwatch.start_next("viper verification"); - verifier.verify(viper_program) + if config::report_viper_messages() { + verify_and_poll_msgs(verifier, context, viper_arc, viper_program, sender) + } else { + verifier.verify(viper_program) + } }) } } } +} + +fn verify_and_poll_msgs( + verifier: &mut viper::Verifier, + verification_context: &viper::VerificationContext, + viper_arc: &Arc, + viper_program: viper::Program, + sender: mpsc::Sender, +) -> VerificationResultKind { + let mut kind = VerificationResultKind::Success; + + // get the reporter global reference outside of the thread scope because it needs to + // be dropped by thread attached to the jvm. This is also why we pass it as reference + // and not per value + let env = &verification_context.env(); + let jni = JniUtils::new(env); + let verifier_wrapper = silver::verifier::Verifier::with(env); + let reporter = jni.unwrap_result(verifier_wrapper.call_reporter(*verifier.verifier_instance())); + let rep_glob_ref = env.new_global_ref(reporter).unwrap(); + + debug!("Starting viper message polling thread"); + + // start thread for polling messages + thread::scope(|scope| { + let polling_thread = scope.spawn(|| polling_function(viper_arc, &rep_glob_ref, sender)); + kind = verifier.verify(viper_program); + polling_thread.join().unwrap(); + }); + debug!("Viper message polling thread terminated"); + kind +} + +fn polling_function( + viper_arc: &Arc, + rep_glob_ref: &jni::objects::GlobalRef, + sender: mpsc::Sender, +) { + let verification_context = viper_arc.attach_current_thread(); + let env = verification_context.env(); + let jni = JniUtils::new(env); + let reporter_instance = rep_glob_ref.as_obj(); + let reporter_wrapper = silver::reporter::PollingReporter::with(env); + loop { + while reporter_wrapper + .call_hasNewMessage(reporter_instance) + .unwrap() + { + let msg = reporter_wrapper + .call_getNewMessage(reporter_instance) + .unwrap(); + debug!("Polling thread received {}", jni.class_name(msg).as_str()); + match jni.class_name(msg).as_str() { + "viper.silver.reporter.VerificationTerminationMessage" => return, + _ => (), + } + } + thread::sleep(time::Duration::from_millis(10)); + } } \ No newline at end of file diff --git a/prusti-server/src/lib.rs b/prusti-server/src/lib.rs index b34b8e235ce..9adde618b8c 100644 --- a/prusti-server/src/lib.rs +++ b/prusti-server/src/lib.rs @@ -188,7 +188,6 @@ fn handle_termination_message( DUMMY_SP.into(), ) .emit(env_diagnostic); - // .emit(&self.env.diagnostic); *overall_result = VerificationResult::Failure; } } diff --git a/prusti-utils/src/config.rs b/prusti-utils/src/config.rs index c59d6d43c46..7651f3bfc0e 100644 --- a/prusti-utils/src/config.rs +++ b/prusti-utils/src/config.rs @@ -103,6 +103,7 @@ lazy_static::lazy_static! { settings.set_default("quiet", false).unwrap(); settings.set_default("assert_timeout", 10_000).unwrap(); settings.set_default("smt_qi_eager_threshold", 1000).unwrap(); + settings.set_default("report_viper_messages", false).unwrap(); settings.set_default("use_more_complete_exhale", true).unwrap(); settings.set_default("skip_unsupported_features", false).unwrap(); settings.set_default("internal_errors_as_warnings", false).unwrap(); @@ -173,6 +174,7 @@ lazy_static::lazy_static! { // Flags specifically for Prusti-Assistant: settings.set_default("show_ide_info", false).unwrap(); settings.set_default("skip_verification", false).unwrap(); + settings.set_default::>("verify_only_defpath", None).unwrap(); // Get the list of all allowed flags. let mut allowed_keys = get_keys(&settings); @@ -506,6 +508,12 @@ pub fn smt_qi_eager_threshold() -> u64 { read_setting("smt_qi_eager_threshold") } +/// Whether to report the messages produced by the viper backend (e.g. quantifier instantiations, +/// quantifier triggers) +pub fn report_viper_messages() -> bool { + read_setting("report_viper_messages") +} + /// Maximum time (in milliseconds) for the verifier to spend on checks. /// Set to None uses the verifier's default value. Maps to the verifier command-line /// argument `--checkTimeout`. @@ -1047,4 +1055,10 @@ pub fn show_ide_info() -> bool { /// of issue #1261 pub fn skip_verification() -> bool { read_setting("skip_verification") +} + +/// Used for selective verification, can be passed a String containing +/// the DefPath of the method to be verified +pub fn verify_only_defpath() -> Option { + read_setting("verify_only_defpath") } \ No newline at end of file diff --git a/prusti/src/callbacks.rs b/prusti/src/callbacks.rs index 022c4cf7f52..b13cd3291d0 100644 --- a/prusti/src/callbacks.rs +++ b/prusti/src/callbacks.rs @@ -29,6 +29,7 @@ use prusti_rustc_interface::{ session::{EarlyErrorHandler, Session}, span::DUMMY_SP, }; +use ::log::debug; #[derive(Default)] pub struct PrustiCompilerCalls; @@ -199,11 +200,32 @@ impl prusti_rustc_interface::driver::Callbacks for PrustiCompilerCalls { // collect and output Information used by IDE: if !config::no_verify() && !config::skip_verification() { - let verification_task = VerificationTask { - procedures: annotated_procedures, - types, - }; - verify(env, def_spec, verification_task); + if let Some(target_def_path) = config::verify_only_defpath() { + // if we do selective verification, then definitely only + // for methods of the primary package. Check needed because + // of the fake_error, otherwise verification stops early + // with local dependencies + if is_primary_package { + let procedures = annotated_procedures + .into_iter() + .filter(|x| env.name.get_unique_item_name(*x) == target_def_path) + .collect(); + debug!("selected procedures: {:?}", procedures); + let selective_task = VerificationTask { procedures, types }; + // fake_error because otherwise a verification-success + // (for a single method for example) will cause this result + // to be cached by compiler at the moment + verify(env, def_spec, selective_task); + // FIXME: problematic because env is moved above + // fake_error(&env); + } + } else { + let verification_task = VerificationTask { + procedures: annotated_procedures, + types, + }; + verify(env, def_spec, verification_task); + } } else if config::skip_verification() && !config::no_verify() && is_primary_package { // add a fake error, reason explained in issue #1261 fake_error(&env);